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.