# Data types¶

A data type declaration consists of:

- The
`type`

keyword, - a unique name for the type,
- the
`:=`

symbol, and - a non-empty list of constructor declarations (functions for building the elements of the data type).

The simplest data type is the `Unit`

type with one constructor called
`unit`

.

```
type Unit := unit : Unit;
```

In the following example, we declare the type `Nat`

– the unary
representation of natural numbers. This type comes with two
constructors: `zero`

and `suc`

. Example elements of type `Nat`

are the
number one represented by `suc zero`

, the number two represented by
`suc (suc zero)`

, etc.

```
type Nat :=
| zero : Nat
| suc : Nat -> Nat;
```

Constructors can be used like normal functions or in patterns when defining functions by pattern matching. For example, here is a function adding two natural numbers:

```
infixl 6 +;
+ : Nat -> Nat -> Nat;
+ zero b := b;
+ (suc a) b := suc (a + b);
```

A data type can possess type parameters. When a data type has a type parameter `A`

, it is referred to as *polymorphic in* `A`

. A classic example of this concept is the `List`

type, which is polymorphic in the type of its list elements.

```
infixr 5 ::;
type List (A : Type) :=
| nil : List A
| :: : A -> List A -> List A;
```

The following function determines whether an element is in a list or not.

```
open import Stdlib.Data.Bool using {Bool;false;||};
elem :
{A : Type} -> (A -> A -> Bool) -> A -> List A -> Bool;
elem _ _ nil := false;
elem eq s (x :: xs) := eq s x || elem eq s xs;
```

For more examples of inductive types and how to use them, see the Juvix standard library.