# Inductive data types

The `inductive`

keyword is reserved for declaring inductive data types.
An inductive type declaration requires a unique name for its type and
its constructors, functions for building its terms. Constructors can be
used as normal identifiers and also in patterns. As shown later, one can
also provide type parameters to widen the family of inductive types one
can define in Juvix.

The simplest inductive type is the `Empty`

type with no constructors.

```
inductive Empty {};
```

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

, the unary
representation of natural numbers. This type comes with two data
constructors, namely `zero`

and `suc`

. A term of the type `Nat`

is the
number one, represented by `suc zero`

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

, etc.

```
inductive Nat {
zero : Nat;
suc : Nat -> Nat;
};
```

The way to use inductive types is by declaring functions by pattern matching. Let us define, for example, the function for adding two natural numbers.

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

As mentioned earlier, an inductive type may have type parameters. The
canonical example is the polymorphic type `List`

. The type `List`

is the
inductive type that considers the type of the elements in the list as a
parameter. A constructor to build the empty list, that is the base case,
and another constructor to enlarge the list, we usually called it
`cons`

. One possible definition for this type is the following type
taken from the Juvix standard library:

```
infixr 5 ∷;
inductive List (A : Type) {
nil : List A;
∷ : A -> List A -> List A;
};
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;
```

To see more examples of inductive types and how to use them, please check out the Juvix standard library