Functions can be introduced by giving a type and a definition. For instance, the polymorphic identity function can be defined by

id : {A : Set} -> A -> A id x = x

Note that the implicit argument is left out in the left hand side. As in a lambda abstraction it can be given explicitly by enclosing it in curly braces:

id : {A : Set} -> A -> A id {A} x = x

Datatypes are introduced by `data`

declarations. For instance, the natural
numbers can be defined by

data Nat : Set where zero : Nat suc : Nat -> Nat

To ensure normalisation, inductive occurrences must appear in strictly positive positions. For instance, the following datatype is not allowed:

```
data Bad : Set where
bad : (Bad -> Bad) -> Bad
```

since there is a negative occurrence of `Bad`

in the argument to the
constructor.

Functions over elements of a datatype can be defined using pattern matching and structural recursion. The addition function on natural numbers is defined by

_+_ : Nat -> Nat -> Nat zero + m = m suc n + m = suc (n + m)

The operator form can be used both in left hand sides and right hand sides as seen here.

Datatypes can be parametrised over a telescope of parameters. These are written after the name of the datatype and scope over the constructors.

data List (A : Set) : Set where [] : List A _::_ : A -> List A -> List A

This will introduce the constructors

[] : {A : Set} -> List A _::_ : {A : Set} -> A -> List A -> List A

We can also define families of datatypes. For
instance, the family over natural numbers `n`

of proofs that `n`

is even.

data IsEven : Nat -> Set where evenZ : IsEven zero evenSS : (n : Nat) -> IsEven n -> IsEven (suc (suc n))

Note the difference between the left and the right side of the first `:`

.
Types appearing on the left are parameters and scope over the constructors.
These have to be unchanged in the return types of the constructors. Types
appearing on the right are indices which are not in scope in the constructors,
and which take on arbitrary values in the constructor return types.

When pattern matching on an element of an inductive family we get information about the index. To distinguish parts of a pattern which are determined by pattern matching (the inaccessible patterns) and the parts which constitutes the actual pattern matching, the inaccessible patterns are prefixed with a dot. In For instance, we can prove that the sum of two even numbers is also even.

even+ : (n m : Nat) -> IsEven n -> IsEven m -> IsEven (n + m) even+ .zero m evenZ em = em even+ .(suc (suc n)) m (evenSS n en) em = evenSS (n + m) (even+ n m en em)

The proof is by recursion on the proof that `n`

is even. Pattern matching on
this proof will force the value of `n`

and hence the patterns for `n`

are
prefixed with a dot to indicate that they are not part of the pattern matching.
In this case we can make `n`

and `m`

implicit and write the proof as

even+ : {n m : Nat} -> IsEven n -> IsEven m -> IsEven (n + m) even+ evenZ em = em even+ (evenSS n en) em = evenSS _ (even+ en em)