module nat where

data nat = zero
         | suc (n : nat)

add : nat -> nat -> nat
add zero m = m
add (suc n) m = suc (add n m)

mul : nat -> nat -> nat
mul zero m = zero
mul (suc n) m = add m (mul n m)

one : nat
one = suc zero

two : nat
two = suc one

three : nat
three = suc two

five : nat
five = add two three

six : nat
six = mul two three