Declarations

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. (The 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

Function declaration

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 x and y.

Postulate declaration

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.

Fixity declaration

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.