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.