CoreSyntax

See the official user manual for the most up-to-date version of the information on this page.

TOC

At its core, Agda is a dependently typed lambda calculus. The grammar of terms is as follows.

 a ::= x         | λ x → a     | a a         | (x : a) → a    | Set[n]   | (a)
       variable  | abstraction | application | function space | universe | grouping

The parentheses for grouping may serve (along with whitespace) to separate tokens. Any amount of extra whitespace between tokens is allowed.

The optional n following Set denotes a level; the default is 0.

Literals are also terms.

TODO: syntax for telescopes.

Terms must be well-scoped and well-typed. To be more precise, see the typing rules.