# 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.