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

instance instOfNat {n : Nat} : OfNat Int 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).

instance Int.instInhabited : Inhabited Int

@[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

@[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

@[defaultInstance 500]

instance Int.instNegInt : Neg Int

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

@[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

instance Int.instAdd : Add Int

@[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

instance Int.instMul : Mul Int

@[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

instance Int.instSub : Sub Int

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.

instance Int.instLEInt : LE Int

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

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

a < b when a + 1 ≤ b.

instance Int.instLTInt : LT Int

@[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

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

@[extern lean_int_dec_nonneg]

def Int.decNonneg (m : Int) : Decidable m.NonNeg

Decides whether an integer is negative.

#eval (7 : Int).decNonneg.decide -- true
#eval (0 : Int).decNonneg.decide -- true
#eval ¬ (-7 : Int).decNonneg.decide -- true

Implemented by efficient native code.

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

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

@[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

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

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

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

@[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

divisibility

instance Int.instDvd : Dvd Int

Divisibility of integers. a ∣ b (typed as \|) says that there is some c such that 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

instance Int.instNatPow : NatPow Int

instance Int.instLawfulBEq : LawfulBEq Int

instance Int.instMin : Min Int

instance Int.instMax : Max Int

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

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

@[simp]

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

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

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