module Constants where open import Sets.Enumerated using (Bool; true; false) open import Sets.Recursive using (ℕ; zero; suc)
Definition of nine with the constructors suc and zero:
nine : ℕ nine = suc (suc (suc (suc (suc (suc (suc (suc (suc zero))))))))
Definition of ten with the help of nine:
ten : ℕ ten = suc nine
The type signature is optional.
ten, suc nine and suc (suc (suc (suc (suc (suc (suc (suc (suc zero)))))))) equally represent the number 10, but only the last one is the so-called normal form.
One can ask for the normal form of an expression in the interactive environment by C-c C-n.