# Notation `ℕ` for the natural numbers. #

source
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 "ℕ")

Instances For