Definition 1.8.1.3.  Let m, n ∈ . We define
m + n
by:
m + (0):= mm + (x+1):= ((m + x)+1)  (x ∈ )
Remarks.

Such inductive definitions are possible due to the definition of natural numbers as a construction (i.e. inductive data type). Note that some of the "+" symbols appearing in this definition are part of the notation of the successor constructor.

References.