Nat type represents the natural numbers, i.e., arbitrary-precision unsigned integers.
There are no overflows.
#eval 100000000000000000 * 200000000000000000000 * 1000000000000000000000
A numeral is considered to be a
Nat if there are no typing constraints.
#check 10 -- Nat #check id 10 -- Nat def f (x : Int) : Int := x - 1 #eval f (3 - 5) -- 3 and 5 are `Int` since `f` expects an `Int`. -- -3
Nat implements truncated subtraction.
#eval 10 - 5 -- 5 #eval 5 - 10 -- 0 theorem ex : 5 - 10 = 0 := rfl #eval (5:Int) - 10 -- -5
Nat implements Euclidean division.
#eval 10 / 4 -- 2 #check 10.0 / 4.0 -- Float #eval 10.0 / 4.0 -- 2.5
As we described in the previous sections, we define the
Nat type as an
namespace hidden inductive Nat where | zero : Nat | succ : Nat → Nat end hidden
However, the internal representation of
Nat is optimized. Small natural numbers (i.e., <
2^63 in a 64-bit machine) are
represented by a single machine word. Big numbers are implemented using GMP numbers.
We recommend you use fixed precision numeric types only in performance critical code.
The Lean kernel has builtin support for the
Nat type too, and can efficiently reduce
Nat expressions during type checking.
#reduce 100000000000000000 * 200000000000000000000 * 1000000000000000000000 theorem ex : 1000000000000000 * 2000000000000000000 = 2000000000000000000000000000000000 := rfl
The sharp-eyed reader will notice that GMP is part of the Lean kernel trusted code base. We believe this is not a problem because you can use external type checkers to double-check your developments, and we consider GMP very trustworthy. Existing external type checkers for Lean 3 (e.g., Trepplein and TC) can be easily adapted to Lean 4. If you are still concerned after checking your development with multiple different external checkers because they may all rely on buggy arbitrary-precision libraries, you can develop your own certified arbitrary-precision library and use it to implement your own type checker for Lean.