Notation ℤ for the integers. #
The type of integers. It is defined as an inductive type based on the
natural number type Nat featuring two constructors: "a natural
number is an integer", and "the negation of a successor of a natural
number is an integer". The former represents integers between 0
(inclusive) and ∞, and the latter integers between -∞ and -1
(inclusive).
This type is special-cased by the compiler. The runtime has a special
representation for Int which stores "small" signed numbers directly,
and larger numbers use an arbitrary precision "bignum" library
(usually GMP). A "small number" is an integer
that can be encoded with 63 bits (31 bits on 32-bits architectures).
Equations
- termℤ = Lean.ParserDescr.node `termℤ 1024 (Lean.ParserDescr.symbol "ℤ")