Documentation

Mathlib.Init.Data.Nat.Notation

Note about Mathlib/Init/ #

The files in Mathlib/Init are leftovers from the port from Mathlib3. (They contain content moved from lean3 itself that Mathlib needed but was not moved to lean4.)

We intend to move all the content of these files out into the main Mathlib directory structure. Contributions assisting with this are appreciated.

#align statements without corresponding declarations (i.e. because the declaration is in Batteries or Lean) can be left here. These will be deleted soon so will not significantly delay deleting otherwise empty Init files.

Notation ℕ for the natural numbers. #

source
def termℕ :
Lean.ParserDescr

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
Instances For