# plfa - Naturals

### How do we define a `Natural`

?

First we observe that it is an `inductive`

type.

It has a base case `zero`

and inductive case `suc`

to get to the next natural.

So we can define it as:

```
data N : Set where
zero : N
suc : N -> N
```

Note here that an inductive definition without a base case is useless, we have nothing to begin with.