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

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

instance instNatCastInt : NatCast Int

Equations

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

instance instOfNat {n : Nat} : OfNat Int n

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 : Inhabited Int

Equations

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

@[simp]

theorem Int.default_eq_zero : default = 0

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 : Nat → Int

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) : 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 : Neg Int

Equations

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

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

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) : 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 : Add Int

Equations

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

@[extern lean_int_mul]

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:

• (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 : Mul Int

Equations

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

@[extern lean_int_sub]

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:

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

Equations

• m.sub n = m + -n

instance Int.instSub : Sub Int

Equations

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

inductive Int.NonNeg : Int → Prop

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) : Prop

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 : LE Int

Equations

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

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

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 : LT Int

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

• (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

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:

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

Equations

• (Int.ofNat n.succ).sign = 1
• (Int.ofNat 0).sign = 0
• (Int.negSucc a).sign = -1

Conversion

def Int.toNat : Int → Nat

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 : Dvd Int

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

Equations

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

instance Int.instNatPow : NatPow Int

Equations

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

instance Int.instLawfulBEq : LawfulBEq Int

instance Int.instMin : Min Int

Equations

• Int.instMin = minOfLe

instance Int.instMax : Max Int

Equations

• Int.instMax = maxOfLe

class IntCast (R : Type u) : 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.

instance instIntCastInt : IntCast Int

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

@[simp]

theorem Int.cast_eq (x : Int) : ↑x = x

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

Equations

• instCoeTailIntOfIntCast = { coe := Int.cast }

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

Equations

• instCoeHTCTIntOfIntCast = { coe := Int.cast }