Notation ℕ for the natural numbers.

def termℕ : Lean.ParserDescr

The natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient implementation. Both use a fast arbitrary-precision arithmetic library (usually GMP); at runtime, Nat values that are sufficiently small are unboxed.

Equations

• termℕ = Lean.ParserDescr.node `termℕ 1024 (Lean.ParserDescr.symbol "ℕ")