The Lean Language Reference

18.2. Integers🔗

The integers are whole numbers, both positive and negative. Integers are arbitrary-precision, limited only by the capability of the hardware on which Lean is running; for fixed-width integers that are used in programming and computer science, please see the section on fixed-precision integers.

Integers are specially supported by Lean's implementation. The logical model of the integers is based on the natural numbers: each integer is modeled as either a natural number or the negative successor of a natural number. Operations on the integers are specified using this model, which is used in the kernel and in interpreted code. In these contexts, integer code inherits the performance benefits of the natural numbers' special support. In compiled code, integers are represented as efficient arbitrary-precision integers, and sufficiently small numbers are stored as unboxed values that don't require indirection through a pointer. Arithmetic operations are implemented by primitives that take advantage of the efficient representations.

18.2.1. Logical Model🔗

Integers are represented either as a natural number or as the negation of the successor of a natural number.

🔗inductive type
Int : Type

The integers.

This type is special-cased by the compiler and overridden with an efficient implementation. The runtime has a special representation for Int that stores “small” signed numbers directly, while larger numbers use a fast arbitrary-precision arithmetic library (usually GMP). A “small number” is an integer that can be encoded with one fewer bits than the platform's pointer size (i.e. 63 bits on 64-bit architectures and 31 bits on 32-bit architectures).

Constructors

ofNat : Nat → Int

A natural number is an integer.

This constructor covers the non-negative integers (from 0 to ∞).

negSucc : Nat → Int

The negation of the successor of a natural number is an integer.

This constructor covers the negative integers (from -1 to -∞).

This representation of the integers has a number of useful properties. It is relatively simple to use and to understand. Unlike a pair of a sign and a Nat, there is a unique representation for 0, which simplifies reasoning about equality. Integers can also be represented as a pair of natural numbers in which one is subtracted from the other, but this requires a quotient type to be well-behaved, and quotient types can be laborious to work with due to the need to prove that functions respect the equivalence relation.

18.2.2. Run-Time Representation🔗

Like natural numbers, sufficiently-small integers are represented as unboxed values: the lowest-order bit in an object pointer is used to indicate that the value is not, in fact, a pointer. If an integer is too large to fit in the remaining bits, it is instead allocated as an ordinary Lean object that consists of an object header and an arbitrary-precision integer.

18.2.3. Syntax🔗

The OfNat Int instance allows numerals to be used as literals, both in expression and in pattern contexts. (OfNat.ofNat n : Int) reduces to the constructor application Int.ofNat n. The Neg Int instance allows negation to be used as well.

On top of these instances, there is special syntax for the constructor Int.negSucc that is available when the Int namespace is opened. The notation -[ n +1] is suggestive of -(n + 1), which is the meaning of Int.negSucc n.

syntaxNegative Successor

-[ n +1] is notation for Int.negSucc n.

term ::= ...
    | `-[n+1]` is suggestive notation for `negSucc n`, which is the second constructor of
`Int` for making strictly negative numbers by mapping `n : Nat` to `-(n + 1)`.
-[ term +1]

18.2.4. API Reference

18.2.4.1. Properties

🔗def
Int.sign : Int → Int

Returns the “sign” of the integer as another integer:

  • 1 for positive numbers,

  • -1 for negative numbers, and

  • 0 for 0.

Examples:

18.2.4.2. Conversions

🔗def
Int.natAbs (m : Int) : Nat

The absolute value of an integer is its distance from 0.

This function is overridden by the compiler with an efficient implementation. This definition is the logical model.

Examples:

🔗def
Int.toNat : Int → Nat

Converts an integer into a natural number. Negative numbers are converted to 0.

Examples:

🔗def
Int.toNat? : Int → Option Nat

Converts an integer into a natural number. Returns none for negative numbers.

Examples:

🔗def
Int.toISize (i : Int) : ISize

Converts an arbitrary-precision integer to a word-sized signed integer, wrapping around on over- or underflow.

This function is overridden at runtime with an efficient implementation.

🔗def
Int.toInt8 (i : Int) : Int8

Converts an arbitrary-precision integer to an 8-bit integer, wrapping on overflow or underflow.

Examples:

🔗def
Int.toInt16 (i : Int) : Int16

Converts an arbitrary-precision integer to a 16-bit integer, wrapping on overflow or underflow.

Examples:

🔗def
Int.toInt32 (i : Int) : Int32

Converts an arbitrary-precision integer to a 32-bit integer, wrapping on overflow or underflow.

Examples:

🔗def
Int.toInt64 (i : Int) : Int64

Converts an arbitrary-precision integer to a 64-bit integer, wrapping on overflow or underflow.

This function is overridden at runtime with an efficient implementation.

Examples:

🔗def
Int.repr : Int → String

Returns the decimal string representation of an integer.

18.2.4.3. Arithmetic

Typically, arithmetic operations on integers are accessed using Lean's overloaded arithmetic notation. In particular, the instances of Add Int, Neg Int, Sub Int, and Mul Int allow ordinary infix operators to be used. Division is somewhat more intricate, because there are multiple sensible notions of division on integers.

🔗def
Int.add (m n : Int) : Int

Addition of integers, usually accessed via the + operator.

This function is overridden by the compiler with an efficient implementation. This definition is the logical model.

Examples:

🔗def
Int.sub (m n : Int) : Int

Subtraction of integers, usually accessed via the - operator.

This function is overridden by the compiler with an efficient implementation. This definition is the logical model.

Examples:

🔗def
Int.subNatNat (m n : Nat) : Int

Non-truncating subtraction of two natural numbers.

Examples:

🔗def
Int.neg (n : Int) : Int

Negation of integers, usually accessed via the - prefix operator.

This function is overridden by the compiler with an efficient implementation. This definition is the logical model.

Examples:

🔗def
Int.negOfNat : Nat → Int

Negation of natural numbers.

Examples:

🔗def
Int.mul (m n : Int) : Int

Multiplication of integers, usually accessed via the * operator.

This function is overridden by the compiler with an efficient implementation. This definition is the logical model.

Examples:

🔗def
Int.pow (m : Int) : Nat → Int

Power of an integer to a natural number, usually accessed via the ^ operator.

Examples:

  • (2 : Int) ^ 4 = 16

  • (10 : Int) ^ 0 = 1

  • (0 : Int) ^ 10 = 0

  • (-7 : Int) ^ 3 = -343

🔗def
Int.gcd (m n : Int) : Nat

Computes the greatest common divisor of two integers as a natural number. The GCD of two integers is the largest natural number that evenly divides both. However, the GCD of a number and 0 is the number's absolute value.

This implementation uses Nat.gcd, which is overridden in both the kernel and the compiler to efficiently evaluate using arbitrary-precision arithmetic.

Examples:

🔗def
Int.lcm (m n : Int) : Nat

Computes the least common multiple of two integers as a natural number. The LCM of two integers is the smallest natural number that's evenly divisible by the absolute values of both.

Examples:

18.2.4.3.1. Division🔗

The Div Int and Mod Int instances implement Euclidean division, described in the reference for Int.ediv. This is not, however, the only sensible convention for rounding and remainders in division. Four pairs of division and modulus functions are available, implementing various conventions.

Division by 0

In all integer division conventions, division by 0 is defined to be 0:

0#eval Int.ediv 5 0 0#eval Int.ediv 0 0 0#eval Int.ediv (-5) 0 0#eval Int.bdiv 5 0 0#eval Int.bdiv 0 0 0#eval Int.bdiv (-5) 0 0#eval Int.fdiv 5 0 0#eval Int.fdiv 0 0 0#eval Int.fdiv (-5) 0 0#eval Int.tdiv 5 0 0#eval Int.tdiv 0 0 0#eval Int.tdiv (-5) 0

All evaluate to 0.

0
🔗def
Int.ediv : Int → Int → Int

Integer division that uses the E-rounding convention. Usually accessed via the / operator. Division by zero is defined to be zero, rather than an error.

In the E-rounding convention (Euclidean division), Int.emod x y satisfies 0 ≤ Int.emod x y < Int.natAbs y for y ≠ 0 and Int.ediv is the unique function satisfying Int.emod x y + (Int.edivx y) * y = x for y ≠ 0.

This means that Int.ediv x y is ⌊x / y⌋ when y > 0 and ⌈x / y⌉ when y < 0.

This function is overridden by the compiler with an efficient implementation. This definition is the logical model.

Examples:

🔗def
Int.emod : Int → Int → Int

Integer modulus that uses the E-rounding convention. Usually accessed via the % operator.

In the E-rounding convention (Euclidean division), Int.emod x y satisfies 0 ≤ Int.emod x y < Int.natAbs y for y ≠ 0 and Int.ediv is the unique function satisfying Int.emod x y + (Int.edivx y) * y = x for y ≠ 0.

This function is overridden by the compiler with an efficient implementation. This definition is the logical model.

Examples:

🔗def
Int.tdiv : Int → Int → Int

Integer division using the T-rounding convention.

In the T-rounding convention (division with truncation), all rounding is towards zero. Division by 0 is defined to be 0. In this convention, Int.tmod a b + b * (Int.tdiv a b) = a.

This function is overridden by the compiler with an efficient implementation. This definition is the logical model.

Examples:

🔗def
Int.tmod : Int → Int → Int

Integer modulo using the T-rounding convention.

In the T-rounding convention (division with truncation), all rounding is towards zero. Division by 0 is defined to be 0 and Int.tmod a 0 = a.

In this convention, Int.tmod a b + b * (Int.tdiv a b) = a. Additionally, Int.natAbs (Int.tmod a b) = Int.natAbs a % Int.natAbs b, and when b does not divide a, Int.tmod a b has the same sign as a.

This function is overridden by the compiler with an efficient implementation. This definition is the logical model.

Examples:

🔗def
Int.bdiv (x : Int) (m : Nat) : Int

Balanced division.

This returns the unique integer so that b * (Int.bdiv a b) + Int.bmod a b = a.

Examples:

🔗def
Int.bmod (x : Int) (m : Nat) : Int

Balanced modulus.

This version of integer modulus uses the balanced rounding convention, which guarantees that -m / 2 ≤ Int.bmod x m < m/2 for m ≠ 0 and Int.bmod x m is congruent to x modulo m.

If m = 0, then Int.bmod x m = x.

Examples:

🔗def
Int.fdiv : Int → Int → Int

Integer division using the F-rounding convention.

In the F-rounding convention (flooring division), Int.fdiv x y satisfies Int.fdiv x y = ⌊x / y⌋ and Int.fmod is the unique function satisfying Int.fmod x y + (Int.fdiv x y) * y = x.

Examples:

🔗def
Int.fmod : Int → Int → Int

Integer modulus using the F-rounding convention.

In the F-rounding convention (flooring division), Int.fdiv x y satisfies Int.fdiv x y = ⌊x / y⌋ and Int.fmod is the unique function satisfying Int.fmod x y + (Int.fdiv x y) * y = x.

Examples:

18.2.4.4. Bitwise Operators

Bitwise operators on Int can be understood as bitwise operators on an infinite stream of bits that are the twos-complement representation of integers.

🔗def
Int.not : Int → Int

Bitwise not, usually accessed via the ~~~ prefix operator.

Interprets the integer as an infinite sequence of bits in two's complement and complements each bit.

Examples:

  • ~~~(0 : Int) = -1

  • ~~~(1 : Int) = -2

  • ~~~(-1 : Int) = 0

🔗def
Int.shiftRight : Int → Nat → Int

Bitwise right shift, usually accessed via the >>> operator.

Interprets the integer as an infinite sequence of bits in two's complement and shifts the value to the right.

Examples:

  • ( 0b0111 : Int) >>> 1 = 0b0011

  • ( 0b1000 : Int) >>> 1 = 0b0100

  • (-0b1000 : Int) >>> 1 = -0b0100

  • (-0b0111 : Int) >>> 1 = -0b0100

18.2.4.5. Comparisons

Equality and inequality tests on Int are typically performed using the decidability of its equality and ordering relations or using the BEq Int and Ord Int instances.

🔗def
Int.le (a b : Int) : Prop

Non-strict inequality of integers, usually accessed via the ≤ operator.

a ≤ b is defined as b - a ≥ 0, using Int.NonNeg.

🔗def
Int.lt (a b : Int) : Prop

Strict inequality of integers, usually accessed via the < operator.

a < b when a + 1 ≤ b.

🔗def
Int.decEq (a b : Int) : Decidable (a = b)

Decides whether two integers are equal. Usually accessed via the DecidableEq Int instance.

This function is overridden by the compiler with an efficient implementation. This definition is the logical model.

Examples: