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 withn
links, which is horribly inefficient. Instead, the runtime itself has a special representation forNat
which stores numbers up to 2^63 directly and larger numbers use an arbitrary precision "bignum" library (usually GMP).
Constructors
-
zero : _root_.Nat
Nat.zero
, is the smallest natural number. This is one of the two constructors ofNat
. UsingNat.zero
should usually be avoided in favor of0 : Nat
or simply0
, in order to remain compatible with the simp normal form defined byNat.zero_eq
. -
succ (n : _root_.Nat) : _root_.Nat
The successor function on natural numbers,
succ n = n + 1
. This is one of the two constructors ofNat
. Usingsucc n
should usually be avoided in favor ofn + 1
, in order to remain compatible with the simp normal form defined byNat.succ_eq_add_one
.