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.