See the official user manual for the most up-to-date version of the information on this page.
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 variable | abstraction | application | function space | universe
Powered by PmWiki