Import list

module Constants where

open import Sets.Enumerated using (Bool; true; false)
open import Sets.Recursive using (; zero; suc)

Constant definitions

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.

Normal form

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.