See the official user manual for the most up-to-date version of the information on this page.
Agda code is written in plain text files consisting of Unicode characters encoded in UTF-8. It is standard practice to make extensive use of Unicode characters for mathematical symbols such as ⊗, ∈, ∅ and so on. There are special shortcuts for entering some of these symbols: see Unicode input. The underscore character plays a special role: see Mixfix. Non-alphanumeric characters often appear as part of variable names. See names for discussion of conventions related to this.
Whitespace is more important than in many other systems. In particular, n+m is a single token, and is not the same as n + m.
Agda programs are organised into modules, with one top-level module per file.
One can also mix Agda code with LaTeX commentary and exposition. This is called literate Agda.