# Integer Type, Coercions, and Notation #

This file defines the Int type as well as

• coercions, conversions, and compatibility with numeric literals,
• a few Nat-related operations such as negOfNat and subNatNat,
• relations </≤/≥/>, the NonNeg property and min/max,
• decidability of equality, relations and NonNeg.
inductive Int :

The type of integers. It is defined as an inductive type based on the natural number type Nat featuring two constructors: "a natural number is an integer", and "the negation of a successor of a natural number is an integer". The former represents integers between 0 (inclusive) and ∞, and the latter integers between -∞ and -1 (inclusive).

This type is special-cased by the compiler. The runtime has a special representation for Int which stores "small" signed numbers directly, and larger numbers use an arbitrary precision "bignum" library (usually GMP). A "small number" is an integer that can be encoded with 63 bits (31 bits on 32-bits architectures).

• ofNat:

A natural number is an integer (0 to ∞).

• negSucc:

The negation of the successor of a natural number is an integer (-1 to -∞).

Instances For
instance instNatCastInt :
Equations
instance instOfNat {n : Nat} :
Equations
• instOfNat = { ofNat := }

-[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.
Instances For
Equations
@[simp]
theorem Int.default_eq_zero :
default = 0

## Coercions #

@[simp]
theorem Int.ofNat_eq_coe {n : Nat} :
= n
@[simp]
theorem Int.ofNat_zero :
0 = 0
@[simp]
theorem Int.ofNat_one :
1 = 1
theorem Int.ofNat_two :
2 = 2

Negation of a natural number.

Equations
Instances For
@[extern lean_int_neg]
def Int.neg (n : Int) :

Negation of an integer.

Implemented by efficient native code.

Equations
Instances For
@[defaultInstance 500]
instance Int.instNegInt :
Equations
def Int.subNatNat (m : Nat) (n : Nat) :

Subtraction of two natural numbers.

Equations
Instances For
def Int.add (m : Int) (n : Int) :

#eval (7 : Int) + (6 : Int) -- 13
#eval (6 : Int) + (-6 : Int) -- 0


Implemented by efficient native code.

Equations
Instances For
Equations
@[extern lean_int_mul]
def Int.mul (m : Int) (n : Int) :

Multiplication of two integers.

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


Implemented by efficient native code.

Equations
Instances For
instance Int.instMul :
Equations
@[extern lean_int_sub]
def Int.sub (m : Int) (n : Int) :

Subtraction of two integers.

#eval (63 : Int) - (6 : Int) -- 57
#eval (7 : Int) - (0 : Int) -- 7
#eval (0 : Int) - (7 : Int) -- -7


Implemented by efficient native code.

Equations
• m.sub n = m + -n
Instances For
instance Int.instSub :
Equations
inductive Int.NonNeg :

A proof that an Int is non-negative.

• mk: ∀ (n : Nat), (Int.ofNat n).NonNeg

Sole constructor, proving that ofNat n is positive.

Instances For
def Int.le (a : Int) (b : Int) :

Definition of a ≤ b, encoded as b - a ≥ 0.

Equations
• a.le b = (b - a).NonNeg
Instances For
instance Int.instLEInt :
Equations
def Int.lt (a : Int) (b : Int) :

Definition of a < b, encoded as a + 1 ≤ b.

Equations
Instances For
instance Int.instLTInt :
Equations
@[extern lean_int_dec_eq]
def Int.decEq (a : Int) (b : Int) :
Decidable (a = b)

Decides equality between two Ints.

#eval (7 : Int) = (3 : Int) + (4 : Int) -- true
#eval (6 : Int) = (3 : Int) * (2 : Int) -- true
#eval ¬ (6 : Int) = (3 : Int) -- true


Implemented by efficient native code.

Equations
Instances For
Equations
@[extern lean_int_dec_le]
instance Int.decLe (a : Int) (b : Int) :

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
@[extern lean_int_dec_lt]
instance Int.decLt (a : Int) (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
@[extern lean_nat_abs]
def Int.natAbs (m : Int) :

Absolute value (Nat) of an integer.

#eval (7 : Int).natAbs -- 7
#eval (0 : Int).natAbs -- 0
#eval (-11 : Int).natAbs -- 11


Implemented by efficient native code.

Equations
Instances For

## sign #

def Int.sign :

Returns the "sign" of the integer as another integer: 1 for positive numbers, -1 for negative numbers, and 0 for 0.

Equations
Instances For

## Conversion #

def Int.toNat :

Turns an integer into a natural number, negative numbers become 0.

#eval (7 : Int).toNat -- 7
#eval (0 : Int).toNat -- 0
#eval (-7 : Int).toNat -- 0

Equations
Instances For
• If n : Nat, then int.toNat' n = some n
• If n : Int is negative, then int.toNat' n = none.
Equations
Instances For

## divisibility #

instance Int.instDvd :

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

Equations

## Powers #

def Int.pow (m : Int) :

Power of an integer to some natural number.

#eval (2 : Int) ^ 4 -- 16
#eval (10 : Int) ^ 0 -- 1
#eval (0 : Int) ^ 10 -- 0
#eval (-7 : Int) ^ 3 -- -343

Equations
• m.pow 0 = 1
• m.pow m_1.succ = m.pow m_1 * m
Instances For
instance Int.instNatPow :
Equations
Equations
instance Int.instMin :
Equations
instance Int.instMax :
Equations
class IntCast (R : Type u) :

The canonical homomorphism Int → R. In most use cases R will have a ring structure and this will be a ring homomorphism.

• intCast : IntR

The canonical map Int → R.

Instances
instance instIntCastInt :
Equations
@[reducible, match_pattern]
def Int.cast {R : Type u} [] :
IntR

Apply the canonical homomorphism from Int to a type R from an IntCast R instance.

In Mathlib there will be such a homomorphism whenever R is an additive group with a 1.

Equations
• Int.cast = IntCast.intCast
Instances For
instance instCoeTailIntOfIntCast {R : Type u_1} [] :
Equations
• instCoeTailIntOfIntCast = { coe := Int.cast }
instance instCoeHTCTIntOfIntCast {R : Type u_1} [] :
Equations
• instCoeHTCTIntOfIntCast = { coe := Int.cast }