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.
The tokens that may appear in source files are literals, names, and keywords. Tokens are separated by whitespace, including comments, and organised into blocks.
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.