plfa - Naturals
How do we define a
First we observe that it is an
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.