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:
Powered by PmWiki