SyntaxOverview

The syntax of an Agda program is defined in terms of three key components:

• Expressions, which are used to write function bodies and types;
• Declarations, which are used to declare types, data-types, postulates, records, functions etc.;
• Pragmas, which are used to define program options.

There are also three levels of syntax, corresponding to differing levels of interpretation:

• Concrete, the high-level sugared syntax, representing exactly what the user wrote (Agda.Syntax.Concrete);
• Abstract, (Agda.Syntax.Abstract);
• Internal, the full-intepreted core Agda terms, roughly corresponding to (Agda.Syntax.Internal).