Documentation

Init.Data.Int.Basic

Integer Type, Coercions, and Notation #

This file defines the Int type as well as

coercions, conversions, and compatibility with numeric literals,
basic arithmetic operations add/sub/mul/pow,
a few Nat-related operations such as negOfNat and subNatNat,
relations </≤/≥/>, the NonNeg property and min/max,
decidability of equality, relations and NonNeg.

Division and modulus operations are defined in Init.Data.Int.DivMod.Basic.

inductive Int :

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).

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 -∞).

Instances For

instance instNatCastInt :

Equations

instNatCastInt = { natCast := fun (n : Nat) => Int.ofNat n }

instance instOfNat {n : Nat} :

Equations

instOfNat = { ofNat := Int.ofNat n }

def Int.«term-[_+1]» :

Lean.ParserDescr

-[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).

Equations

One or more equations did not get rendered due to their size.

instance Int.instInhabited :

Equations

Int.instInhabited = { default := Int.ofNat 0 }

@[simp]

theorem Int.default_eq_zero :

theorem Int.zero_ne_one :

0 ≠ 1

Coercions #

@[simp]

theorem Int.ofNat_eq_coe {n : Nat} :

ofNat n = ↑n

@[simp]

theorem Int.ofNat_zero :

↑0 = 0

@[simp]

theorem Int.ofNat_one :

↑1 = 1

theorem Int.ofNat_two :

↑2 = 2

def Int.negOfNat :

Negation of natural numbers.

Examples:

Int.negOfNat 6 = -6
Int.negOfNat 0 = 0

Equations

Int.negOfNat 0 = 0
Int.negOfNat m.succ = Int.negSucc m

@[extern lean_int_neg]

def Int.neg (n : 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:

-(6 : Int) = -6
-(-6 : Int) = 6
(12 : Int).neg = -12

Equations

(Int.ofNat n_2).neg = Int.negOfNat n_2
(Int.negSucc n_2).neg = ↑n_2.succ

@[defaultInstance 500]

instance Int.instNegInt :

Equations

Int.instNegInt = { neg := Int.neg }

def Int.subNatNat (m n : Nat) :

Non-truncating subtraction of two natural numbers.

Examples:

Int.subNatNat 5 2 = 3
Int.subNatNat 2 5 = -3
Int.subNatNat 0 13 = -13

Equations

Int.subNatNat m n = match n - m with | 0 => Int.ofNat (m - n) | k.succ => Int.negSucc k

@[extern lean_int_add]

def Int.add (m n : 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:

(7 : Int) + (6 : Int) = 13
(6 : Int) + (-6 : Int) = 0

Equations

(Int.ofNat m_2).add (Int.ofNat n_2) = Int.ofNat (m_2 + n_2)
(Int.ofNat m_2).add (Int.negSucc n_2) = Int.subNatNat m_2 n_2.succ
(Int.negSucc m_2).add (Int.ofNat n_2) = Int.subNatNat n_2 m_2.succ
(Int.negSucc m_2).add (Int.negSucc n_2) = Int.negSucc (m_2 + n_2).succ

instance Int.instAdd :

Equations

Int.instAdd = { add := Int.add }

@[extern lean_int_mul]

def Int.mul (m n : 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:

(63 : Int) * (6 : Int) = 378
(6 : Int) * (-6 : Int) = -36
(7 : Int) * (0 : Int) = 0

Equations

(Int.ofNat m_2).mul (Int.ofNat n_2) = Int.ofNat (m_2 * n_2)
(Int.ofNat m_2).mul (Int.negSucc n_2) = Int.negOfNat (m_2 * n_2.succ)
(Int.negSucc m_2).mul (Int.ofNat n_2) = Int.negOfNat (m_2.succ * n_2)
(Int.negSucc m_2).mul (Int.negSucc n_2) = Int.ofNat (m_2.succ * n_2.succ)

instance Int.instMul :

Equations

Int.instMul = { mul := Int.mul }

@[extern lean_int_sub]

def Int.sub (m n : 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:

(63 : Int) - (6 : Int) = 57
(7 : Int) - (0 : Int) = 7
(0 : Int) - (7 : Int) = -7

Equations

m.sub n = m + -n

instance Int.instSub :

Equations

Int.instSub = { sub := Int.sub }

inductive Int.NonNeg :

An integer is non-negative if it is equal to a natural number.

mk (n : Nat) : (ofNat n).NonNeg
For all natural numbers n, Int.ofNat n is non-negative.

def Int.le (a b : Int) :

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

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

Equations

a.le b = (b - a).NonNeg

instance Int.instLEInt :

Equations

Int.instLEInt = { le := Int.le }

def Int.lt (a b : Int) :

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

a < b when a + 1 ≤ b.

Equations

a.lt b = (a + 1 ≤ b)

instance Int.instLTInt :

Equations

Int.instLTInt = { lt := Int.lt }

@[extern lean_int_dec_eq]

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:

show (7 : Int) = (3 : Int) + (4 : Int) by decide
if (6 : Int) = (3 : Int) * (2 : Int) then "yes" else "no" = "yes"
(¬ (6 : Int) = (3 : Int)) = true

Equations

(Int.ofNat m_1).decEq (Int.ofNat n_1) = match decEq m_1 n_1 with | isTrue h => isTrue ⋯ | isFalse h => isFalse ⋯
(Int.ofNat m_1).decEq (Int.negSucc n_1) = isFalse ⋯
(Int.negSucc m_1).decEq (Int.ofNat n_1) = isFalse ⋯
(Int.negSucc m_1).decEq (Int.negSucc n_1) = match decEq m_1 n_1 with | isTrue h => isTrue ⋯ | isFalse h => isFalse ⋯

instance Int.instDecidableEq :

DecidableEq Int

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:

show (7 : Int) = (3 : Int) + (4 : Int) by decide
if (6 : Int) = (3 : Int) * (2 : Int) then "yes" else "no" = "yes"
(¬ (6 : Int) = (3 : Int)) = true

Equations

Int.instDecidableEq = Int.decEq

@[extern lean_int_dec_le]

instance Int.decLe (a b : Int) :

Decidable (a ≤ b)

Decides whether a ≤ b.

#eval ¬ ( (7 : Int) ≤ (0 : Int) ) -- true
#eval (0 : Int) ≤ (0 : Int) -- true
#eval (7 : Int) ≤ (10 : Int) -- true

Implemented by efficient native code.

Equations

a.decLe b = Int.decNonneg✝ (b - a)

@[extern lean_int_dec_lt]

instance Int.decLt (a b : Int) :

Decidable (a < b)

Decides whether a < b.

#eval `¬ ( (7 : Int) < 0 )` -- true
#eval `¬ ( (0 : Int) < 0 )` -- true
#eval `(7 : Int) < 10` -- true

Implemented by efficient native code.

Equations

a.decLt b = Int.decNonneg✝ (b - (a + 1))

@[extern lean_nat_abs]

def Int.natAbs (m : Int) :

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:

(7 : Int).natAbs = 7
(0 : Int).natAbs = 0
((-11 : Int).natAbs = 11

Equations

(Int.ofNat n_1).natAbs = n_1
(Int.negSucc n_1).natAbs = n_1.succ

sign #

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

1 for positive numbers,
-1 for negative numbers, and
0 for 0.

Examples:

Int.sign 34 = 1
Int.sign 2 = 1
Int.sign 0 = 0
Int.sign -1 = -1
Int.sign -362 = -1

Equations

Conversion #

def Int.toNat :

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

Examples:

(7 : Int).toNat = 7
(0 : Int).toNat = 0
(-7 : Int).toNat = 0

Equations

(Int.ofNat n).toNat = n
(Int.negSucc a).toNat = 0

def Int.toNat? :

Int → Option Nat

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

Examples:

(7 : Int).toNat? = some 7
(0 : Int).toNat? = some 0
(-7 : Int).toNat? = none

Equations

(Int.ofNat n).toNat? = some n
(Int.negSucc a).toNat? = none

@[reducible, inline, deprecated Int.toNat? (since := "2025-03-11")]

abbrev Int.toNat' :

Int → Option Nat

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

Examples:

(7 : Int).toNat? = some 7
(0 : Int).toNat? = some 0
(-7 : Int).toNat? = none

Equations

Int.toNat' = Int.toNat?

divisibility #

instance Int.instDvd :

Divisibility of integers. a ∣ b (typed as \|) says that there is some c such that b = a * c.

Equations

Int.instDvd = { dvd := fun (a b : Int) => ∃ (c : Int ), b = a * c }

Powers #

def Int.pow (m : 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

Equations

m.pow 0 = 1
m.pow m_1.succ = m.pow m_1 * m

instance Int.instNatPow :

Equations

Int.instNatPow = { pow := Int.pow }

instance Int.instLawfulBEq :

instance Int.instMin :

Equations

Int.instMin = minOfLe

instance Int.instMax :

Equations

Int.instMax = maxOfLe

class IntCast (R : Type u) :

The canonical homomorphism Int → R. In most use cases, the target type will have a ring structure, and this homomorphism should be a ring homomorphism.

IntCast and NatCast exist to allow different libraries with their own types that can be notated as natural numbers to have consistent simp normal forms without needing to create coercion simplification sets that are aware of all combinations. Libraries should make it easy to work with IntCast where possible. For instance, in Mathlib there will be such a homomorphism (and thus an IntCast R instance) whenever R is an additive group with a 1.

intCast : Int → R
The canonical map Int → R.

Instances

instance instIntCastInt :

Equations

instIntCastInt = { intCast := fun (n : Int) => n }

@[reducible, match_pattern]

def Int.cast {R : Type u} [IntCast R] :

Int → R

The canonical homomorphism Int → R. In most use cases, the target type will have a ring structure, and this homomorphism should be a ring homomorphism.

IntCast and NatCast exist to allow different libraries with their own types that can be notated as natural numbers to have consistent simp normal forms without needing to create coercion simplification sets that are aware of all combinations. Libraries should make it easy to work with IntCast where possible. For instance, in Mathlib there will be such a homomorphism (and thus an IntCast R instance) whenever R is an additive group with a 1.

Equations

Int.cast = IntCast.intCast

instance instCoeTailIntOfIntCast {R : Type u_1} [IntCast R] :

Equations

instCoeTailIntOfIntCast = { coe := Int.cast }

instance instCoeHTCTIntOfIntCast {R : Type u_1} [IntCast R] :

Equations

instCoeHTCTIntOfIntCast = { coe := Int.cast }