Integers

The Int type represents the arbitrary-precision integers. There are no overflows.

#eval (100000000000000000 : Int) * 200000000000000000000 * 1000000000000000000000

Recall that nonnegative numerals are considered to be a Nat if there are no typing constraints.

#check 1 -- Nat
#check -1 -- Int
#check (1:Int) -- Int

The operator / for Int implements integer division.

#eval -10 / 4 -- -2

Similar to Nat, the internal representation of Int is optimized. Small integers are represented by a single machine word. Big integers are implemented using GMP numbers. We recommend you use fixed precision numeric types only in performance critical code.

The Lean kernel does not have special support for reducing Int during type checking. However, since Int is defined as

# namespace hidden
inductive Int : Type where
  | ofNat   : Nat → Int
  | negSucc : Nat → Int
# end hidden

the type checker will be able reduce Int expressions efficiently by relying on the special support for Nat.

theorem ex : -2000000000 * 1000000000 = -2000000000000000000 :=
 rfl