Definition 1.8.1.2 (Positional notation).

We write:

  • 0 := $"Natural numbers".zero
  • 1 := $"Natural numbers".successor(n = $number(value = 0))
  • 2 := $"Natural numbers".successor(n = $number(value = 1))
  • 3 := $"Natural numbers".successor(n = $number(value = 2))
  • ...
Remarks.

Positional notation is implemented as a macro, i.e. using additional code that is injected into the proof checker. Therefore, no definition is given here.

References.