See the official user manual for the most up-to-date version of the information on this page.
A program in Agda consists of a number of declarations. A declaration introduces a new identifier and gives its type and definition. It is possible to declare data types, functions, records, postulates, and fixity.
Declarations have a signature part and a definition part.
These can appear separately.
Names must be declared before they are used, but by separating the signature from the definition it is possible to define things in mutual recursion.
mutual keyword is deprecated and not necessary.)
Inductive data type declaration
Introduces a name of a new (co-)inductively defined type and names for its constructors. For instance, the set of natural numbers is defined by:
data Nat : Set where zero : Nat suc : Nat -> Nat
Introduces a name of a new function together with its type and definition. For instance, the addition function is defined by:
add : Nat -> Nat -> Nat add zero m = m add (suc n) m = suc (add n m)
Record type declaration
Introduces a name for a new record type. For instance, the declaration
record Point : Set where field x : Nat y : Nat
declares a record type
Point with two natural number fields
Introduces a name for an object of a given type. This also postulates the existence of that object, since it is possible to refer to it by its name. A simple example is:
postulate A : Set a : A
which postulates that the set
A exists and that it has the element
a. The use of postulates can easily result in logical inconsistencies. For example, we can postulate an element in the empty type.
Defines a precedence and associativity (left, right, or not associative) for an operator. A simple example is:
infixl 5 _+_
which declares the name _+_ to be left associative with a precedence of 5.