# Notation `ℕ`

for the natural numbers. #

The type of natural numbers, starting at zero. It is defined as an inductive type freely generated by "zero is a natural number" and "the successor of a natural number is a natural number".

You can prove a theorem `P n`

about `n : Nat`

by `induction n`

, which will
expect a proof of the theorem for `P 0`

, and a proof of `P (succ i)`

assuming
a proof of `P i`

. The same method also works to define functions by recursion
on natural numbers: induction and recursion are two expressions of the same
operation from Lean's point of view.

```
open Nat
example (n : Nat) : n < succ n := by
induction n with
| zero =>
show 0 < 1
decide
| succ i ih => -- ih : i < succ i
show succ i < succ (succ i)
exact Nat.succ_lt_succ ih
```

This type is special-cased by both the kernel and the compiler:

- The type of expressions contains "
`Nat`

literals" as a primitive constructor, and the kernel knows how to reduce zero/succ expressions to nat literals. - If implemented naively, this type would represent a numeral
`n`

in unary as a linked list with`n`

links, which is horribly inefficient. Instead, the runtime itself has a special representation for`Nat`

which stores numbers up to 2^63 directly and larger numbers use an arbitrary precision "bignum" library (usually GMP).

## Equations

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