Syntax Overview

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).