# 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 "ℤ")