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.

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.

Equations

• Int.sign x = match x with | Int.ofNat (Nat.succ n) => 1 | Int.ofNat 0 => 0 | Int.negSucc a => -1

toNat'

def Int.toNat' : Int → Option Nat

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

Equations

• Int.toNat' x = match x with | Int.ofNat n => some n | Int.negSucc a => none

Quotient and remainder

There are three main conventions for integer division, referred here as the E, F, T rounding conventions. All three pairs satisfy the identity x % y + (x / y) * y = x unconditionally, and satisfy x / 0 = 0 and x % 0 = x.

E-rounding division

This pair satisfies 0 ≤ mod x y < natAbs y for y ≠ 0.

def Int.ediv : Int → Int → Int

Integer division. This version of Int.div uses the E-rounding convention (euclidean division), in which Int.emod x y satisfies 0 ≤ mod x y < natAbs y for y ≠ 0 and Int.ediv is the unique function satisfying emod x y + (ediv x y) * y = x.

Equations

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

def Int.emod : Int → Int → Int

Integer modulus. This version of Int.mod uses the E-rounding convention (euclidean division), in which Int.emod x y satisfies 0 ≤ emod x y < natAbs y for y ≠ 0 and Int.ediv is the unique function satisfying emod x y + (ediv x y) * y = x.

Equations

• Int.emod x✝ x = match x✝, x with | Int.ofNat m, n => Int.ofNat (m % Int.natAbs n) | Int.negSucc m, n => Int.subNatNat (Int.natAbs n) (Nat.succ (m % Int.natAbs n))

F-rounding division

This pair satisfies fdiv x y = floor (x / y).

def Int.fdiv : Int → Int → Int

Integer division. This version of Int.div uses the F-rounding convention (flooring division), in which Int.fdiv x y satisfies fdiv x y = floor (x / y) and Int.fmod is the unique function satisfying fmod x y + (fdiv x y) * y = x.

Equations

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

def Int.fmod : Int → Int → Int

Integer modulus. This version of Int.mod uses the F-rounding convention (flooring division), in which Int.fdiv x y satisfies fdiv x y = floor (x / y) and Int.fmod is the unique function satisfying fmod x y + (fdiv x y) * y = x.

Equations

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

T-rounding division

This pair satisfies div x y = round_to_zero (x / y). Int.div and Int.mod are defined in core lean.

instance Int.instDivInt_1 : Div Int

Core Lean provides instances using T-rounding division, i.e. Int.div and Int.mod. We override these here.

Equations

• Int.instDivInt_1 = { div := Int.ediv }

instance Int.instModInt_1 : Mod Int

Equations

• Int.instModInt_1 = { mod := Int.emod }

gcd

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

Computes the greatest common divisor of two integers, as a Nat.

Equations

• Int.gcd m n = Nat.gcd (Int.natAbs m) (Int.natAbs n)

divisibility

instance Int.instDvdInt : Dvd Int

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

Equations

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

bit operations

def Int.not : Int → Int

Bitwise not

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

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

Equations

• Int.not x = match x with | Int.ofNat n => Int.negSucc n | Int.negSucc n => Int.ofNat n

instance Int.instComplementInt : Complement Int

Equations

• Int.instComplementInt = { complement := Int.not }

def Int.shiftRight : Int → Nat → Int

Bitwise shift right.

Conceptually, this treats the integer as an infinite sequence of bits in two's complement and shifts the value to the right.

( 0b0111:Int) >>> 1 =  0b0011
( 0b1000:Int) >>> 1 =  0b0100
(-0b1000:Int) >>> 1 = -0b0100
(-0b0111:Int) >>> 1 = -0b0100

Equations

• Int.shiftRight x✝ x = match x✝, x with | Int.ofNat n, s => Int.ofNat (n >>> s) | Int.negSucc n, s => Int.negSucc (n >>> s)

instance Int.instHShiftRightIntNat : HShiftRight Int Nat Int

Equations

• Int.instHShiftRightIntNat = { hShiftRight := Int.shiftRight }

instance Int.instToExprInt : Lean.ToExpr Int

Equations

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