This module contains the definition of signed fixed width integer types as well as basic arithmetic and bitwise operations on top of it.

structure Int8 : Type

Signed 8-bit integers.

This type has special support in the compiler so it can be represented by an unboxed 8-bit value.

• ofUInt8 :: (
• toUInt8 : UInt8

  Converts an 8-bit signed integer into the 8-bit unsigned integer that is its two's complement encoding.

• )

Instances For

• Int8.instNeg
• Int8.instOfNat
• Lean.instToExprInt8
• Std.Int8.instLawfulEqOrdInt8
• Std.Int8.instTransOrdInt8
• instAddInt8
• instAndOpInt8
• instComplementInt8
• instDivInt8
• instHashableInt8
• instInhabitedInt8
• instLEInt8
• instLTInt8
• instMaxInt8
• instMinInt8
• instModInt8
• instMulInt8
• instOrOpInt8
• instOrdInt8
• instReprAtomInt8
• instReprInt8
• instShiftLeftInt8
• instShiftRightInt8
• instSubInt8
• instToStringInt8
• instXorInt8

structure Int16 : Type

Signed 16-bit integers.

This type has special support in the compiler so it can be represented by an unboxed 16-bit value.

• ofUInt16 :: (
• toUInt16 : UInt16

  Converts an 16-bit signed integer into the 16-bit unsigned integer that is its two's complement encoding.

• )

Instances For

• Int16.instNeg
• Int16.instOfNat
• Lean.instToExprInt16
• Std.Int16.instLawfulEqOrdInt16
• Std.Int16.instTransOrdInt16
• instAddInt16
• instAndOpInt16
• instComplementInt16
• instDivInt16
• instHashableInt16
• instInhabitedInt16
• instLEInt16
• instLTInt16
• instMaxInt16
• instMinInt16
• instModInt16
• instMulInt16
• instOrOpInt16
• instOrdInt16
• instReprAtomInt16
• instReprInt16
• instShiftLeftInt16
• instShiftRightInt16
• instSubInt16
• instToStringInt16
• instXorInt16

structure Int32 : Type

Signed 32-bit integers.

This type has special support in the compiler so it can be represented by an unboxed 32-bit value.

• ofUInt32 :: (
• toUInt32 : UInt32

  Converts an 32-bit signed integer into the 32-bit unsigned integer that is its two's complement encoding.

• )

Instances For

• Int32.instNeg
• Int32.instOfNat
• Lean.instToExprInt32
• Std.Int32.instLawfulEqOrdInt32
• Std.Int32.instTransOrdInt32
• instAddInt32
• instAndOpInt32
• instComplementInt32
• instDivInt32
• instHashableInt32
• instInhabitedInt32
• instLEInt32
• instLTInt32
• instMaxInt32
• instMinInt32
• instModInt32
• instMulInt32
• instOrOpInt32
• instOrdInt32
• instReprAtomInt32
• instReprInt32
• instShiftLeftInt32
• instShiftRightInt32
• instSubInt32
• instToStringInt32
• instXorInt32

structure Int64 : Type

Signed 64-bit integers.

This type has special support in the compiler so it can be represented by an unboxed 64-bit value.

• ofUInt64 :: (
• toUInt64 : UInt64

  Converts an 64-bit signed integer into the 64-bit unsigned integer that is its two's complement encoding.

• )

Instances For

• Int64.instNeg
• Int64.instOfNat
• Lean.instToExprInt64
• Std.Int64.instLawfulEqOrdInt64
• Std.Int64.instTransOrdInt64
• instAddInt64
• instAndOpInt64
• instComplementInt64
• instDivInt64
• instHashableInt64
• instInhabitedInt64
• instLEInt64
• instLTInt64
• instMaxInt64
• instMinInt64
• instModInt64
• instMulInt64
• instOrOpInt64
• instOrdInt64
• instReprAtomInt64
• instReprInt64
• instShiftLeftInt64
• instShiftRightInt64
• instSubInt64
• instToStringInt64
• instXorInt64

structure ISize : Type

Signed integers that are the size of a word on the platform's architecture.

On a 32-bit architecture, ISize is equivalent to Int32. On a 64-bit machine, it is equivalent to Int64. This type has special support in the compiler so it can be represented by an unboxed value.

• ofUSize :: (
• toUSize : USize

  Converts a word-sized signed integer into the word-sized unsigned integer that is its two's complement encoding.

• )

Instances For

• ISize.instNeg
• ISize.instOfNat
• Lean.instToExprISize
• Std.ISize.instLawfulEqOrdISize
• Std.ISize.instTransOrdISize
• instAddISize
• instAndOpISize
• instComplementISize
• instDivISize
• instHashableISize
• instInhabitedISize
• instLEISize
• instLTISize
• instMaxISize
• instMinISize
• instModISize
• instMulISize
• instOrOpISize
• instOrdISize
• instReprAtomISize
• instReprISize
• instShiftLeftISize
• instShiftRightISize
• instSubISize
• instToStringISize
• instXorISize

@[reducible, inline]

abbrev Int8.size : Nat

The number of distinct values representable by Int8, that is, 2^8 = 256.

Equations

• Int8.size = 256

@[inline]

def Int8.toBitVec (x : Int8) : BitVec 8

Obtain the BitVec that contains the 2's complement representation of the Int8.

Equations

• x.toBitVec = x.toUInt8.toBitVec

theorem Int8.toBitVec.inj {x y : Int8} : x.toBitVec = y.toBitVec → x = y

@[inline]

def UInt8.toInt8 (i : UInt8) : Int8

Obtains the Int8 that is 2's complement equivalent to the UInt8.

Equations

• i.toInt8 = { toUInt8 := i }

@[inline, deprecated UInt8.toInt8 (since := "2025-02-13")]

def Int8.mk (i : UInt8) : Int8

Obtains the Int8 that is 2's complement equivalent to the UInt8.

Equations

• Int8.mk i = i.toInt8

@[extern lean_int8_of_int]

def Int8.ofInt (i : Int) : Int8

Converts an arbitrary-precision integer to an 8-bit integer, wrapping on overflow or underflow.

This function is overridden at runtime with an efficient implementation.

Examples:

• Int8.ofInt 48 = 48
• Int8.ofInt (-115) = -115
• Int8.ofInt (-129) = 127
• Int8.ofInt (128) = -128

Equations

• Int8.ofInt i = { toUInt8 := { toBitVec := BitVec.ofInt 8 i } }

@[extern lean_int8_of_nat]

def Int8.ofNat (n : Nat) : Int8

Converts a natural number to an 8-bit signed integer, wrapping around on overflow.

This function is overridden at runtime with an efficient implementation.

Examples:

• Int8.ofNat 53 = 53
• Int8.ofNat 127 = 127
• Int8.ofNat 128 = -128
• Int8.ofNat 255 = -1

Equations

• Int8.ofNat n = { toUInt8 := { toBitVec := BitVec.ofNat 8 n } }

@[reducible, inline]

abbrev Int.toInt8 (i : Int) : Int8

Converts an arbitrary-precision integer to an 8-bit integer, wrapping on overflow or underflow.

Examples:

• Int.toInt8 48 = 48
• Int.toInt8 (-115) = -115
• Int.toInt8 (-129) = 127
• Int.toInt8 (128) = -128

Equations

• Int.toInt8 = Int8.ofInt

@[reducible, inline]

abbrev Nat.toInt8 (n : Nat) : Int8

Converts a natural number to an 8-bit signed integer, wrapping around to negative numbers on overflow.

Examples:

• Nat.toInt8 53 = 53
• Nat.toInt8 127 = 127
• Nat.toInt8 128 = -128
• Nat.toInt8 255 = -1

Equations

• Nat.toInt8 = Int8.ofNat

@[extern lean_int8_to_int]

def Int8.toInt (i : Int8) : Int

Converts an 8-bit signed integer to an arbitrary-precision integer that denotes the same number.

This function is overridden at runtime with an efficient implementation.

Equations

• i.toInt = i.toBitVec.toInt

@[inline]

def Int8.toNatClampNeg (i : Int8) : Nat

Converts an 8-bit signed integer to a natural number, mapping all negative numbers to 0.

Use Int8.toBitVec to obtain the two's complement representation.

Equations

• i.toNatClampNeg = i.toInt.toNat

@[inline, deprecated Int8.toNatClampNeg (since := "2025-02-13")]

def Int8.toNat (i : Int8) : Nat

Converts an 8-bit signed integer to a natural number, mapping all negative numbers to 0.

Use Int8.toBitVec to obtain the two's complement representation.

Equations

• i.toNat = i.toInt.toNat

@[inline]

def Int8.ofBitVec (b : BitVec 8) : Int8

Obtains the Int8 whose 2's complement representation is the given BitVec 8.

Equations

• Int8.ofBitVec b = { toUInt8 := { toBitVec := b } }

@[extern lean_int8_neg]

def Int8.neg (i : Int8) : Int8

Negates 8-bit signed integers. Usually accessed via the - prefix operator.

This function is overridden at runtime with an efficient implementation.

Equations

• i.neg = { toUInt8 := { toBitVec := -i.toBitVec } }

instance instToStringInt8 : ToString Int8

Equations

• instToStringInt8 = { toString := fun (i : Int8) => toString i.toInt }

instance instReprInt8 : Repr Int8

Equations

• instReprInt8 = { reprPrec := fun (i : Int8) (prec : Nat) => reprPrec i.toInt prec }

instance instReprAtomInt8 : ReprAtom Int8

Equations

• instReprAtomInt8 = { }

instance instHashableInt8 : Hashable Int8

Equations

• instHashableInt8 = { hash := fun (i : Int8) => i.toUInt8.toUInt64 }

instance Int8.instOfNat {n : Nat} : OfNat Int8 n

Equations

• Int8.instOfNat = { ofNat := Int8.ofNat n }

instance Int8.instNeg : Neg Int8

Equations

• Int8.instNeg = { neg := Int8.neg }

@[reducible, inline]

abbrev Int8.maxValue : Int8

The largest number that Int8 can represent: 2^7 - 1 = 127.

Equations

• Int8.maxValue = 127

@[reducible, inline]

abbrev Int8.minValue : Int8

The smallest number that Int8 can represent: -2^7 = -128.

Equations

• Int8.minValue = -128

@[inline]

def Int8.ofIntLE (i : Int) (_hl : minValue.toInt ≤ i) (_hr : i ≤ maxValue.toInt) : Int8

Constructs an Int8 from an Int that is known to be in bounds.

Equations

• Int8.ofIntLE i _hl _hr = Int8.ofInt i

def Int8.ofIntTruncate (i : Int) : Int8

Constructs an Int8 from an Int, clamping if the value is too small or too large.

Equations

• Int8.ofIntTruncate i = if hl : Int8.minValue.toInt ≤ i then if hr : i ≤ Int8.maxValue.toInt then Int8.ofIntLE i hl hr else Int8.minValue else Int8.minValue

@[extern lean_int8_add]

def Int8.add (a b : Int8) : Int8

Adds two 8-bit signed integers, wrapping around on over- or underflow. Usually accessed via the + operator.

This function is overridden at runtime with an efficient implementation.

Equations

• a.add b = { toUInt8 := { toBitVec := a.toBitVec + b.toBitVec } }

@[extern lean_int8_sub]

def Int8.sub (a b : Int8) : Int8

Subtracts one 8-bit signed integer from another, wrapping around on over- or underflow. Usually accessed via the - operator.

This function is overridden at runtime with an efficient implementation.

Equations

• a.sub b = { toUInt8 := { toBitVec := a.toBitVec - b.toBitVec } }

@[extern lean_int8_mul]

def Int8.mul (a b : Int8) : Int8

Multiplies two 8-bit signed integers, wrapping around on over- or underflow. Usually accessed via the * operator.

This function is overridden at runtime with an efficient implementation.

Equations

• a.mul b = { toUInt8 := { toBitVec := a.toBitVec * b.toBitVec } }

@[extern lean_int8_div]

def Int8.div (a b : Int8) : Int8

Truncating division for 8-bit signed integers, rounding towards zero. Usually accessed via the / operator.

Division by zero is defined to be zero.

This function is overridden at runtime with an efficient implementation.

Examples:

• Int8.div 10 3 = 3
• Int8.div 10 (-3) = (-3)
• Int8.div (-10) (-3) = 3
• Int8.div (-10) 3 = (-3)
• Int8.div 10 0 = 0

Equations

• a.div b = { toUInt8 := { toBitVec := a.toBitVec.sdiv b.toBitVec } }

@[extern lean_int8_mod]

def Int8.mod (a b : Int8) : Int8

The modulo operator for 8-bit signed integers, which computes the remainder when dividing one integer by another with the T-rounding convention used by Int8.div. Usually accessed via the % operator.

When the divisor is 0, the result is the dividend rather than an error.

This function is overridden at runtime with an efficient implementation.

Examples:

• Int8.mod 5 2 = 1
• Int8.mod 5 (-2) = 1
• Int8.mod (-5) 2 = (-1)
• Int8.mod (-5) (-2) = (-1)
• Int8.mod 4 2 = 0
• Int8.mod 4 (-2) = 0
• Int8.mod 4 0 = 4
• Int8.mod (-4) 0 = (-4)

Equations

• a.mod b = { toUInt8 := { toBitVec := a.toBitVec.srem b.toBitVec } }

@[extern lean_int8_land]

def Int8.land (a b : Int8) : Int8

Bitwise and for 8-bit signed integers. Usually accessed via the &&& operator.

Each bit of the resulting integer is set if the corresponding bits of both input integers are set, according to the two's complement representation.

This function is overridden at runtime with an efficient implementation.

Equations

• a.land b = { toUInt8 := { toBitVec := a.toBitVec &&& b.toBitVec } }

@[extern lean_int8_lor]

def Int8.lor (a b : Int8) : Int8

Bitwise or for 8-bit signed integers. Usually accessed via the ||| operator.

Each bit of the resulting integer is set if at least one of the corresponding bits of the input integers is set, according to the two's complement representation.

This function is overridden at runtime with an efficient implementation.

Equations

• a.lor b = { toUInt8 := { toBitVec := a.toBitVec ||| b.toBitVec } }

@[extern lean_int8_xor]

def Int8.xor (a b : Int8) : Int8

Bitwise exclusive or for 8-bit signed integers. Usually accessed via the ^^^ operator.

Each bit of the resulting integer is set if exactly one of the corresponding bits of the input integers is set, according to the two's complement representation.

This function is overridden at runtime with an efficient implementation.

Equations

• a.xor b = { toUInt8 := { toBitVec := a.toBitVec ^^^ b.toBitVec } }

@[extern lean_int8_shift_left]

def Int8.shiftLeft (a b : Int8) : Int8

Bitwise left shift for 8-bit signed integers. Usually accessed via the <<< operator.

Signed integers are interpreted as bitvectors according to the two's complement representation.

This function is overridden at runtime with an efficient implementation.

Equations

• a.shiftLeft b = { toUInt8 := { toBitVec := a.toBitVec <<< b.toBitVec.smod 8 } }

@[extern lean_int8_shift_right]

def Int8.shiftRight (a b : Int8) : Int8

Arithmetic right shift for 8-bit signed integers. Usually accessed via the <<< operator.

The high bits are filled with the value of the most significant bit.

This function is overridden at runtime with an efficient implementation.

Equations

• a.shiftRight b = { toUInt8 := { toBitVec := a.toBitVec.sshiftRight' (b.toBitVec.smod 8) } }

@[extern lean_int8_complement]

def Int8.complement (a : Int8) : Int8

Bitwise complement, also known as bitwise negation, for 8-bit signed integers. Usually accessed via the ~~~ prefix operator.

Each bit of the resulting integer is the opposite of the corresponding bit of the input integer. Integers use the two's complement representation, so Int8.complement a = -(a + 1).

This function is overridden at runtime with an efficient implementation.

Equations

• a.complement = { toUInt8 := { toBitVec := ~~~a.toBitVec } }

@[extern lean_int8_abs]

def Int8.abs (a : Int8) : Int8

Computes the absolute value of an 8-bit signed integer.

This function is equivalent to if a < 0 then -a else a, so in particular Int8.minValue will be mapped to Int8.minValue.

This function is overridden at runtime with an efficient implementation.

Equations

• a.abs = { toUInt8 := { toBitVec := a.toBitVec.abs } }

@[extern lean_int8_dec_eq]

def Int8.decEq (a b : Int8) : Decidable (a = b)

Decides whether two 8-bit signed integers are equal. Usually accessed via the DecidableEq Int8 instance.

This function is overridden at runtime with an efficient implementation.

Examples:

• Int8.decEq 123 123 = .isTrue rfl
• (if ((-7) : Int8) = 7 then "yes" else "no") = "no"
• show (7 : Int8) = 7 by decide

Equations

• { toUInt8 := n }.decEq { toUInt8 := m } = if h : n = m then isTrue ⋯ else isFalse ⋯

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

Strict inequality of 8-bit signed integers, defined as inequality of the corresponding integers. Usually accessed via the < operator.

Equations

• a.lt b = (a.toBitVec.slt b.toBitVec = true)

def Int8.le (a b : Int8) : Prop

Non-strict inequality of 8-bit signed integers, defined as inequality of the corresponding integers. Usually accessed via the ≤ operator.

Equations

• a.le b = (a.toBitVec.sle b.toBitVec = true)

instance instInhabitedInt8 : Inhabited Int8

Equations

• instInhabitedInt8 = { default := 0 }

instance instAddInt8 : Add Int8

Equations

• instAddInt8 = { add := Int8.add }

instance instSubInt8 : Sub Int8

Equations

• instSubInt8 = { sub := Int8.sub }

instance instMulInt8 : Mul Int8

Equations

• instMulInt8 = { mul := Int8.mul }

instance instModInt8 : Mod Int8

Equations

• instModInt8 = { mod := Int8.mod }

instance instDivInt8 : Div Int8

Equations

• instDivInt8 = { div := Int8.div }

instance instLTInt8 : LT Int8

Equations

• instLTInt8 = { lt := Int8.lt }

instance instLEInt8 : LE Int8

Equations

• instLEInt8 = { le := Int8.le }

instance instComplementInt8 : Complement Int8

Equations

• instComplementInt8 = { complement := Int8.complement }

instance instAndOpInt8 : AndOp Int8

Equations

• instAndOpInt8 = { and := Int8.land }

instance instOrOpInt8 : OrOp Int8

Equations

• instOrOpInt8 = { or := Int8.lor }

instance instXorInt8 : Xor Int8

Equations

• instXorInt8 = { xor := Int8.xor }

instance instShiftLeftInt8 : ShiftLeft Int8

Equations

• instShiftLeftInt8 = { shiftLeft := Int8.shiftLeft }

instance instShiftRightInt8 : ShiftRight Int8

Equations

• instShiftRightInt8 = { shiftRight := Int8.shiftRight }

instance instDecidableEqInt8 : DecidableEq Int8

Equations

• instDecidableEqInt8 = Int8.decEq

@[extern lean_bool_to_int8]

def Bool.toInt8 (b : Bool) : Int8

Converts true to 1 and false to 0.

Equations

• b.toInt8 = if b = true then 1 else 0

@[extern lean_int8_dec_lt]

def Int8.decLt (a b : Int8) : Decidable (a < b)

Decides whether one 8-bit signed integer is strictly less than another. Usually accessed via the DecidableLT Int8 instance.

This function is overridden at runtime with an efficient implementation.

Examples:

• (if ((-7) : Int8) < 7 then "yes" else "no") = "yes"
• (if (5 : Int8) < 5 then "yes" else "no") = "no"
• show ¬((7 : Int8) < 7) by decide

Equations

• a.decLt b = inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec = true))

@[extern lean_int8_dec_le]

def Int8.decLe (a b : Int8) : Decidable (a ≤ b)

Decides whether one 8-bit signed integer is less than or equal to another. Usually accessed via the DecidableLE Int8 instance.

This function is overridden at runtime with an efficient implementation.

Examples:

• (if ((-7) : Int8) ≤ 7 then "yes" else "no") = "yes"
• (if (15 : Int8) ≤ 15 then "yes" else "no") = "yes"
• (if (15 : Int8) ≤ 5 then "yes" else "no") = "no"
• show (7 : Int8) ≤ 7 by decide

Equations

• a.decLe b = inferInstanceAs (Decidable (a.toBitVec.sle b.toBitVec = true))

instance instDecidableLtInt8 (a b : Int8) : Decidable (a < b)

Equations

• instDecidableLtInt8 a b = a.decLt b

instance instDecidableLeInt8 (a b : Int8) : Decidable (a ≤ b)

Equations

• instDecidableLeInt8 a b = a.decLe b

instance instMaxInt8 : Max Int8

Equations

• instMaxInt8 = maxOfLe

instance instMinInt8 : Min Int8

Equations

• instMinInt8 = minOfLe

@[reducible, inline]

abbrev Int16.size : Nat

The number of distinct values representable by Int16, that is, 2^16 = 65536.

Equations

• Int16.size = 65536

@[inline]

def Int16.toBitVec (x : Int16) : BitVec 16

Obtain the BitVec that contains the 2's complement representation of the Int16.

Equations

• x.toBitVec = x.toUInt16.toBitVec

theorem Int16.toBitVec.inj {x y : Int16} : x.toBitVec = y.toBitVec → x = y

@[inline]

def UInt16.toInt16 (i : UInt16) : Int16

Obtains the Int16 that is 2's complement equivalent to the UInt16.

Equations

• i.toInt16 = { toUInt16 := i }

@[inline, deprecated UInt16.toInt16 (since := "2025-02-13")]

def Int16.mk (i : UInt16) : Int16

Obtains the Int16 that is 2's complement equivalent to the UInt16.

Equations

• Int16.mk i = i.toInt16

@[extern lean_int16_of_int]

def Int16.ofInt (i : Int) : Int16

Converts an arbitrary-precision integer to a 16-bit signed integer, wrapping on overflow or underflow.

This function is overridden at runtime with an efficient implementation.

Examples:

• Int16.ofInt 48 = 48
• Int16.ofInt (-129) = -129
• Int16.ofInt (128) = 128
• Int16.ofInt 70000 = 4464
• Int16.ofInt (-40000) = 25536

Equations

• Int16.ofInt i = { toUInt16 := { toBitVec := BitVec.ofInt 16 i } }

@[extern lean_int16_of_nat]

def Int16.ofNat (n : Nat) : Int16

Converts a natural number to a 16-bit signed integer, wrapping around on overflow.

This function is overridden at runtime with an efficient implementation.

Examples:

• Int16.ofNat 127 = 127
• Int16.ofNat 32767 = 32767
• Int16.ofNat 32768 = -32768
• Int16.ofNat 32770 = -32766

Equations

• Int16.ofNat n = { toUInt16 := { toBitVec := BitVec.ofNat 16 n } }

@[reducible, inline]

abbrev Int.toInt16 (i : Int) : Int16

Converts an arbitrary-precision integer to a 16-bit integer, wrapping on overflow or underflow.

Examples:

• Int.toInt16 48 = 48
• Int.toInt16 (-129) = -129
• Int.toInt16 (128) = 128
• Int.toInt16 70000 = 4464
• Int.toInt16 (-40000) = 25536

Equations

• Int.toInt16 = Int16.ofInt

@[reducible, inline]

abbrev Nat.toInt16 (n : Nat) : Int16

Converts a natural number to a 16-bit signed integer, wrapping around to negative numbers on overflow.

Examples:

• Nat.toInt16 127 = 127
• Nat.toInt16 32767 = 32767
• Nat.toInt16 32768 = -32768
• Nat.toInt16 32770 = -32766

Equations

• Nat.toInt16 = Int16.ofNat

@[extern lean_int16_to_int]

def Int16.toInt (i : Int16) : Int

Converts a 16-bit signed integer to an arbitrary-precision integer that denotes the same number.

This function is overridden at runtime with an efficient implementation.

Equations

• i.toInt = i.toBitVec.toInt

@[inline]

def Int16.toNatClampNeg (i : Int16) : Nat

Converts a 16-bit signed integer to a natural number, mapping all negative numbers to 0.

Use Int16.toBitVec to obtain the two's complement representation.

Equations

• i.toNatClampNeg = i.toInt.toNat

@[inline, deprecated Int16.toNatClampNeg (since := "2025-02-13")]

def Int16.toNat (i : Int16) : Nat

Converts a 16-bit signed integer to a natural number, mapping all negative numbers to 0.

Use Int16.toBitVec to obtain the two's complement representation.

Equations

• i.toNat = i.toInt.toNat

@[inline]

def Int16.ofBitVec (b : BitVec 16) : Int16

Obtains the Int16 whose 2's complement representation is the given BitVec 16.

Equations

• Int16.ofBitVec b = { toUInt16 := { toBitVec := b } }

@[extern lean_int16_to_int8]

def Int16.toInt8 (a : Int16) : Int8

Converts 16-bit signed integers to 8-bit signed integers by truncating their bitvector representation.

This function is overridden at runtime with an efficient implementation.

Equations

• a.toInt8 = { toUInt8 := { toBitVec := BitVec.signExtend 8 a.toBitVec } }

@[extern lean_int8_to_int16]

def Int8.toInt16 (a : Int8) : Int16

Converts 8-bit signed integers to 16-bit signed integers that denote the same number.

This function is overridden at runtime with an efficient implementation.

Equations

• a.toInt16 = { toUInt16 := { toBitVec := BitVec.signExtend 16 a.toBitVec } }

@[extern lean_int16_neg]

def Int16.neg (i : Int16) : Int16

Negates 16-bit signed integers. Usually accessed via the - prefix operator.

This function is overridden at runtime with an efficient implementation.

Equations

• i.neg = { toUInt16 := { toBitVec := -i.toBitVec } }

instance instToStringInt16 : ToString Int16

Equations

• instToStringInt16 = { toString := fun (i : Int16) => toString i.toInt }

instance instReprInt16 : Repr Int16

Equations

• instReprInt16 = { reprPrec := fun (i : Int16) (prec : Nat) => reprPrec i.toInt prec }

instance instReprAtomInt16 : ReprAtom Int16

Equations

• instReprAtomInt16 = { }

instance instHashableInt16 : Hashable Int16

Equations

• instHashableInt16 = { hash := fun (i : Int16) => i.toUInt16.toUInt64 }

instance Int16.instOfNat {n : Nat} : OfNat Int16 n

Equations

• Int16.instOfNat = { ofNat := Int16.ofNat n }

instance Int16.instNeg : Neg Int16

Equations

• Int16.instNeg = { neg := Int16.neg }

@[reducible, inline]

abbrev Int16.maxValue : Int16

The largest number that Int16 can represent: 2^15 - 1 = 32767.

Equations

• Int16.maxValue = 32767

@[reducible, inline]

abbrev Int16.minValue : Int16

The smallest number that Int16 can represent: -2^15 = -32768.

Equations

• Int16.minValue = -32768

@[inline]

def Int16.ofIntLE (i : Int) (_hl : minValue.toInt ≤ i) (_hr : i ≤ maxValue.toInt) : Int16

Constructs an Int16 from an Int that is known to be in bounds.

Equations

• Int16.ofIntLE i _hl _hr = Int16.ofInt i

def Int16.ofIntTruncate (i : Int) : Int16

Constructs an Int16 from an Int, clamping if the value is too small or too large.

Equations

• Int16.ofIntTruncate i = if hl : Int16.minValue.toInt ≤ i then if hr : i ≤ Int16.maxValue.toInt then Int16.ofIntLE i hl hr else Int16.minValue else Int16.minValue

@[extern lean_int16_add]

def Int16.add (a b : Int16) : Int16

Adds two 16-bit signed integers, wrapping around on over- or underflow. Usually accessed via the + operator.

This function is overridden at runtime with an efficient implementation.

Equations

• a.add b = { toUInt16 := { toBitVec := a.toBitVec + b.toBitVec } }

@[extern lean_int16_sub]

def Int16.sub (a b : Int16) : Int16

Subtracts one 16-bit signed integer from another, wrapping around on over- or underflow. Usually accessed via the - operator.

This function is overridden at runtime with an efficient implementation.

Equations

• a.sub b = { toUInt16 := { toBitVec := a.toBitVec - b.toBitVec } }

@[extern lean_int16_mul]

def Int16.mul (a b : Int16) : Int16

Multiplies two 16-bit signed integers, wrapping around on over- or underflow. Usually accessed via the * operator.

This function is overridden at runtime with an efficient implementation.

Equations

• a.mul b = { toUInt16 := { toBitVec := a.toBitVec * b.toBitVec } }

@[extern lean_int16_div]

def Int16.div (a b : Int16) : Int16

Truncating division for 16-bit signed integers, rounding towards zero. Usually accessed via the / operator.

Division by zero is defined to be zero.

This function is overridden at runtime with an efficient implementation.

Examples:

• Int16.div 10 3 = 3
• Int16.div 10 (-3) = (-3)
• Int16.div (-10) (-3) = 3
• Int16.div (-10) 3 = (-3)
• Int16.div 10 0 = 0

Equations

• a.div b = { toUInt16 := { toBitVec := a.toBitVec.sdiv b.toBitVec } }

@[extern lean_int16_mod]

def Int16.mod (a b : Int16) : Int16

The modulo operator for 16-bit signed integers, which computes the remainder when dividing one integer by another with the T-rounding convention used by Int16.div. Usually accessed via the % operator.

When the divisor is 0, the result is the dividend rather than an error.

This function is overridden at runtime with an efficient implementation.

Examples:

• Int16.mod 5 2 = 1
• Int16.mod 5 (-2) = 1
• Int16.mod (-5) 2 = (-1)
• Int16.mod (-5) (-2) = (-1)
• Int16.mod 4 2 = 0
• Int16.mod 4 (-2) = 0
• Int16.mod 4 0 = 4
• Int16.mod (-4) 0 = (-4)

Equations

• a.mod b = { toUInt16 := { toBitVec := a.toBitVec.srem b.toBitVec } }

@[extern lean_int16_land]

def Int16.land (a b : Int16) : Int16

Bitwise and for 16-bit signed integers. Usually accessed via the &&& operator.

Each bit of the resulting integer is set if the corresponding bits of both input integers are set, according to the two's complement representation.

This function is overridden at runtime with an efficient implementation.

Equations

• a.land b = { toUInt16 := { toBitVec := a.toBitVec &&& b.toBitVec } }

@[extern lean_int16_lor]

def Int16.lor (a b : Int16) : Int16

Bitwise or for 16-bit signed integers. Usually accessed via the ||| operator.

Each bit of the resulting integer is set if at least one of the corresponding bits of the input integers is set, according to the two's complement representation.

This function is overridden at runtime with an efficient implementation.

Equations

• a.lor b = { toUInt16 := { toBitVec := a.toBitVec ||| b.toBitVec } }

@[extern lean_int16_xor]

def Int16.xor (a b : Int16) : Int16

Bitwise exclusive or for 16-bit signed integers. Usually accessed via the ^^^ operator.

Each bit of the resulting integer is set if exactly one of the corresponding bits of the input integers is set, according to the two's complement representation.

This function is overridden at runtime with an efficient implementation.

Equations

• a.xor b = { toUInt16 := { toBitVec := a.toBitVec ^^^ b.toBitVec } }

@[extern lean_int16_shift_left]

def Int16.shiftLeft (a b : Int16) : Int16

Bitwise left shift for 16-bit signed integers. Usually accessed via the <<< operator.

Signed integers are interpreted as bitvectors according to the two's complement representation.

This function is overridden at runtime with an efficient implementation.

Equations

• a.shiftLeft b = { toUInt16 := { toBitVec := a.toBitVec <<< b.toBitVec.smod 16 } }

@[extern lean_int16_shift_right]

def Int16.shiftRight (a b : Int16) : Int16

Arithmetic right shift for 16-bit signed integers. Usually accessed via the <<< operator.

The high bits are filled with the value of the most significant bit.

This function is overridden at runtime with an efficient implementation.

Equations

• a.shiftRight b = { toUInt16 := { toBitVec := a.toBitVec.sshiftRight' (b.toBitVec.smod 16) } }

@[extern lean_int16_complement]

def Int16.complement (a : Int16) : Int16

Bitwise complement, also known as bitwise negation, for 16-bit signed integers. Usually accessed via the ~~~ prefix operator.

Each bit of the resulting integer is the opposite of the corresponding bit of the input integer. Integers use the two's complement representation, so Int16.complement a = -(a + 1).

This function is overridden at runtime with an efficient implementation.

Equations

• a.complement = { toUInt16 := { toBitVec := ~~~a.toBitVec } }

@[extern lean_int16_abs]

def Int16.abs (a : Int16) : Int16

Computes the absolute value of a 16-bit signed integer.

This function is equivalent to if a < 0 then -a else a, so in particular Int16.minValue will be mapped to Int16.minValue.

This function is overridden at runtime with an efficient implementation.

Equations

• a.abs = { toUInt16 := { toBitVec := a.toBitVec.abs } }

@[extern lean_int16_dec_eq]

def Int16.decEq (a b : Int16) : Decidable (a = b)

Decides whether two 16-bit signed integers are equal. Usually accessed via the DecidableEq Int16 instance.

This function is overridden at runtime with an efficient implementation.

Examples:

• Int16.decEq 123 123 = .isTrue rfl
• (if ((-7) : Int16) = 7 then "yes" else "no") = "no"
• show (7 : Int16) = 7 by decide

Equations

• { toUInt16 := n }.decEq { toUInt16 := m } = if h : n = m then isTrue ⋯ else isFalse ⋯

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

Strict inequality of 16-bit signed integers, defined as inequality of the corresponding integers. Usually accessed via the < operator.

Equations

• a.lt b = (a.toBitVec.slt b.toBitVec = true)

def Int16.le (a b : Int16) : Prop

Non-strict inequality of 16-bit signed integers, defined as inequality of the corresponding integers. Usually accessed via the ≤ operator.

Equations

• a.le b = (a.toBitVec.sle b.toBitVec = true)

instance instInhabitedInt16 : Inhabited Int16

Equations

• instInhabitedInt16 = { default := 0 }

instance instAddInt16 : Add Int16

Equations

• instAddInt16 = { add := Int16.add }

instance instSubInt16 : Sub Int16

Equations

• instSubInt16 = { sub := Int16.sub }

instance instMulInt16 : Mul Int16

Equations

• instMulInt16 = { mul := Int16.mul }

instance instModInt16 : Mod Int16

Equations

• instModInt16 = { mod := Int16.mod }

instance instDivInt16 : Div Int16

Equations

• instDivInt16 = { div := Int16.div }

instance instLTInt16 : LT Int16

Equations

• instLTInt16 = { lt := Int16.lt }

instance instLEInt16 : LE Int16

Equations

• instLEInt16 = { le := Int16.le }

instance instComplementInt16 : Complement Int16

Equations

• instComplementInt16 = { complement := Int16.complement }

instance instAndOpInt16 : AndOp Int16

Equations

• instAndOpInt16 = { and := Int16.land }

instance instOrOpInt16 : OrOp Int16

Equations

• instOrOpInt16 = { or := Int16.lor }

instance instXorInt16 : Xor Int16

Equations

• instXorInt16 = { xor := Int16.xor }

instance instShiftLeftInt16 : ShiftLeft Int16

Equations

• instShiftLeftInt16 = { shiftLeft := Int16.shiftLeft }

instance instShiftRightInt16 : ShiftRight Int16

Equations

• instShiftRightInt16 = { shiftRight := Int16.shiftRight }

instance instDecidableEqInt16 : DecidableEq Int16

Equations

• instDecidableEqInt16 = Int16.decEq

@[extern lean_bool_to_int16]

def Bool.toInt16 (b : Bool) : Int16

Converts true to 1 and false to 0.

Equations

• b.toInt16 = if b = true then 1 else 0

@[extern lean_int16_dec_lt]

def Int16.decLt (a b : Int16) : Decidable (a < b)

Decides whether one 16-bit signed integer is strictly less than another. Usually accessed via the DecidableLT Int16 instance.

This function is overridden at runtime with an efficient implementation.

Examples:

• (if ((-7) : Int16) < 7 then "yes" else "no") = "yes"
• (if (5 : Int16) < 5 then "yes" else "no") = "no"
• show ¬((7 : Int16) < 7) by decide

Equations

• a.decLt b = inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec = true))

@[extern lean_int16_dec_le]

def Int16.decLe (a b : Int16) : Decidable (a ≤ b)

Decides whether one 16-bit signed integer is less than or equal to another. Usually accessed via the DecidableLE Int16 instance.

This function is overridden at runtime with an efficient implementation.

Examples:

• (if ((-7) : Int16) ≤ 7 then "yes" else "no") = "yes"
• (if (15 : Int16) ≤ 15 then "yes" else "no") = "yes"
• (if (15 : Int16) ≤ 5 then "yes" else "no") = "no"
• show (7 : Int16) ≤ 7 by decide

Equations

• a.decLe b = inferInstanceAs (Decidable (a.toBitVec.sle b.toBitVec = true))

instance instDecidableLtInt16 (a b : Int16) : Decidable (a < b)

Equations

• instDecidableLtInt16 a b = a.decLt b

instance instDecidableLeInt16 (a b : Int16) : Decidable (a ≤ b)

Equations

• instDecidableLeInt16 a b = a.decLe b

instance instMaxInt16 : Max Int16

Equations

• instMaxInt16 = maxOfLe

instance instMinInt16 : Min Int16

Equations

• instMinInt16 = minOfLe

@[reducible, inline]

abbrev Int32.size : Nat

The number of distinct values representable by Int32, that is, 2^32 = 4294967296.

Equations

• Int32.size = 4294967296

@[inline]

def Int32.toBitVec (x : Int32) : BitVec 32

Obtain the BitVec that contains the 2's complement representation of the Int32.

Equations

• x.toBitVec = x.toUInt32.toBitVec

theorem Int32.toBitVec.inj {x y : Int32} : x.toBitVec = y.toBitVec → x = y

@[inline]

def UInt32.toInt32 (i : UInt32) : Int32

Obtains the Int32 that is 2's complement equivalent to the UInt32.

Equations

• i.toInt32 = { toUInt32 := i }

@[inline, deprecated UInt32.toInt32 (since := "2025-02-13")]

def Int32.mk (i : UInt32) : Int32

Obtains the Int32 that is 2's complement equivalent to the UInt32.

Equations

• Int32.mk i = i.toInt32

@[extern lean_int32_of_int]

def Int32.ofInt (i : Int) : Int32

Converts an arbitrary-precision integer to a 32-bit integer, wrapping on overflow or underflow.

This function is overridden at runtime with an efficient implementation.

Examples:

• Int32.ofInt 48 = 48
• Int32.ofInt (-129) = -129
• Int32.ofInt 70000 = 70000
• Int32.ofInt (-40000) = -40000
• Int32.ofInt 2147483648 = -2147483648
• Int32.ofInt (-2147483649) = 2147483647

Equations

• Int32.ofInt i = { toUInt32 := { toBitVec := BitVec.ofInt 32 i } }

@[extern lean_int32_of_nat]

def Int32.ofNat (n : Nat) : Int32

Converts a natural number to a 32-bit signed integer, wrapping around on overflow.

This function is overridden at runtime with an efficient implementation.

Examples:

• Int32.ofNat 127 = 127
• Int32.ofNat 32770 = 32770
• Int32.ofNat 2_147_483_647 = 2_147_483_647
• Int32.ofNat 2_147_483_648 = -2_147_483_648

Equations

• Int32.ofNat n = { toUInt32 := { toBitVec := BitVec.ofNat 32 n } }

@[reducible, inline]

abbrev Int.toInt32 (i : Int) : Int32

Converts an arbitrary-precision integer to a 32-bit integer, wrapping on overflow or underflow.

Examples:

• Int.toInt32 48 = 48
• Int.toInt32 (-129) = -129
• Int.toInt32 70000 = 70000
• Int.toInt32 (-40000) = -40000
• Int.toInt32 2147483648 = -2147483648
• Int.toInt32 (-2147483649) = 2147483647

Equations

• Int.toInt32 = Int32.ofInt

@[reducible, inline]

abbrev Nat.toInt32 (n : Nat) : Int32

Converts a natural number to a 32-bit signed integer, wrapping around to negative numbers on overflow.

Examples:

• Nat.toInt32 127 = 127
• Nat.toInt32 32770 = 32770
• Nat.toInt32 2_147_483_647 = 2_147_483_647
• Nat.toInt32 2_147_483_648 = -2_147_483_648

Equations

• Nat.toInt32 = Int32.ofNat

@[extern lean_int32_to_int]

def Int32.toInt (i : Int32) : Int

Converts a 32-bit signed integer to an arbitrary-precision integer that denotes the same number.

This function is overridden at runtime with an efficient implementation.

Equations

• i.toInt = i.toBitVec.toInt

@[inline]

def Int32.toNatClampNeg (i : Int32) : Nat

Converts a 32-bit signed integer to a natural number, mapping all negative numbers to 0.

Use Int32.toBitVec to obtain the two's complement representation.

Equations

• i.toNatClampNeg = i.toInt.toNat

@[inline, deprecated Int32.toNatClampNeg (since := "2025-02-13")]

def Int32.toNat (i : Int32) : Nat

Converts a 32-bit signed integer to a natural number, mapping all negative numbers to 0.

Use Int32.toBitVec to obtain the two's complement representation.

Equations

• i.toNat = i.toInt.toNat

@[inline]

def Int32.ofBitVec (b : BitVec 32) : Int32

Obtains the Int32 whose 2's complement representation is the given BitVec 32.

Equations

• Int32.ofBitVec b = { toUInt32 := { toBitVec := b } }

@[extern lean_int32_to_int8]

def Int32.toInt8 (a : Int32) : Int8

Converts a 32-bit signed integer to an 8-bit signed integer by truncating its bitvector representation.

This function is overridden at runtime with an efficient implementation.

Equations

• a.toInt8 = { toUInt8 := { toBitVec := BitVec.signExtend 8 a.toBitVec } }

@[extern lean_int32_to_int16]

def Int32.toInt16 (a : Int32) : Int16

Converts a 32-bit signed integer to an 16-bit signed integer by truncating its bitvector representation.

This function is overridden at runtime with an efficient implementation.

Equations

• a.toInt16 = { toUInt16 := { toBitVec := BitVec.signExtend 16 a.toBitVec } }

@[extern lean_int8_to_int32]

def Int8.toInt32 (a : Int8) : Int32

Converts 8-bit signed integers to 32-bit signed integers that denote the same number.

This function is overridden at runtime with an efficient implementation.

Equations

• a.toInt32 = { toUInt32 := { toBitVec := BitVec.signExtend 32 a.toBitVec } }

@[extern lean_int16_to_int32]

def Int16.toInt32 (a : Int16) : Int32

Converts 8-bit signed integers to 32-bit signed integers that denote the same number.

This function is overridden at runtime with an efficient implementation.

Equations

• a.toInt32 = { toUInt32 := { toBitVec := BitVec.signExtend 32 a.toBitVec } }

@[extern lean_int32_neg]

def Int32.neg (i : Int32) : Int32

Negates 32-bit signed integers. Usually accessed via the - prefix operator.

This function is overridden at runtime with an efficient implementation.

Equations

• i.neg = { toUInt32 := { toBitVec := -i.toBitVec } }

instance instToStringInt32 : ToString Int32

Equations

• instToStringInt32 = { toString := fun (i : Int32) => toString i.toInt }

instance instReprInt32 : Repr Int32

Equations

• instReprInt32 = { reprPrec := fun (i : Int32) (prec : Nat) => reprPrec i.toInt prec }

instance instReprAtomInt32 : ReprAtom Int32

Equations

• instReprAtomInt32 = { }

instance instHashableInt32 : Hashable Int32

Equations

• instHashableInt32 = { hash := fun (i : Int32) => i.toUInt32.toUInt64 }

instance Int32.instOfNat {n : Nat} : OfNat Int32 n

Equations

• Int32.instOfNat = { ofNat := Int32.ofNat n }

instance Int32.instNeg : Neg Int32

Equations

• Int32.instNeg = { neg := Int32.neg }

@[reducible, inline]

abbrev Int32.maxValue : Int32

The largest number that Int32 can represent: 2^31 - 1 = 2147483647.

Equations

• Int32.maxValue = 2147483647

@[reducible, inline]

abbrev Int32.minValue : Int32

The smallest number that Int32 can represent: -2^31 = -2147483648.

Equations

• Int32.minValue = -2147483648

@[inline]

def Int32.ofIntLE (i : Int) (_hl : minValue.toInt ≤ i) (_hr : i ≤ maxValue.toInt) : Int32

Constructs an Int32 from an Int that is known to be in bounds.

Equations

• Int32.ofIntLE i _hl _hr = Int32.ofInt i

def Int32.ofIntTruncate (i : Int) : Int32

Constructs an Int32 from an Int, clamping if the value is too small or too large.

Equations

• Int32.ofIntTruncate i = if hl : Int32.minValue.toInt ≤ i then if hr : i ≤ Int32.maxValue.toInt then Int32.ofIntLE i hl hr else Int32.minValue else Int32.minValue

@[extern lean_int32_add]

def Int32.add (a b : Int32) : Int32

Adds two 32-bit signed integers, wrapping around on over- or underflow. Usually accessed via the + operator.

This function is overridden at runtime with an efficient implementation.

Equations

• a.add b = { toUInt32 := { toBitVec := a.toBitVec + b.toBitVec } }

@[extern lean_int32_sub]

def Int32.sub (a b : Int32) : Int32

Subtracts one 32-bit signed integer from another, wrapping around on over- or underflow. Usually accessed via the - operator.

This function is overridden at runtime with an efficient implementation.

Equations

• a.sub b = { toUInt32 := { toBitVec := a.toBitVec - b.toBitVec } }

@[extern lean_int32_mul]

def Int32.mul (a b : Int32) : Int32

Multiplies two 32-bit signed integers, wrapping around on over- or underflow. Usually accessed via the * operator.

This function is overridden at runtime with an efficient implementation.

Equations

• a.mul b = { toUInt32 := { toBitVec := a.toBitVec * b.toBitVec } }

@[extern lean_int32_div]

def Int32.div (a b : Int32) : Int32

Truncating division for 32-bit signed integers, rounding towards zero. Usually accessed via the / operator.

Division by zero is defined to be zero.

This function is overridden at runtime with an efficient implementation.

Examples:

• Int32.div 10 3 = 3
• Int32.div 10 (-3) = (-3)
• Int32.div (-10) (-3) = 3
• Int32.div (-10) 3 = (-3)
• Int32.div 10 0 = 0

Equations

• a.div b = { toUInt32 := { toBitVec := a.toBitVec.sdiv b.toBitVec } }

@[extern lean_int32_mod]

def Int32.mod (a b : Int32) : Int32

The modulo operator for 32-bit signed integers, which computes the remainder when dividing one integer by another with the T-rounding convention used by Int32.div. Usually accessed via the % operator.

When the divisor is 0, the result is the dividend rather than an error.

This function is overridden at runtime with an efficient implementation.

Examples:

• Int32.mod 5 2 = 1
• Int32.mod 5 (-2) = 1
• Int32.mod (-5) 2 = (-1)
• Int32.mod (-5) (-2) = (-1)
• Int32.mod 4 2 = 0
• Int32.mod 4 (-2) = 0
• Int32.mod 4 0 = 4
• Int32.mod (-4) 0 = (-4)

Equations

• a.mod b = { toUInt32 := { toBitVec := a.toBitVec.srem b.toBitVec } }

@[extern lean_int32_land]

def Int32.land (a b : Int32) : Int32

Bitwise and for 32-bit signed integers. Usually accessed via the &&& operator.

Each bit of the resulting integer is set if the corresponding bits of both input integers are set, according to the two's complement representation.

This function is overridden at runtime with an efficient implementation.

Equations

• a.land b = { toUInt32 := { toBitVec := a.toBitVec &&& b.toBitVec } }

@[extern lean_int32_lor]

def Int32.lor (a b : Int32) : Int32

Bitwise or for 32-bit signed integers. Usually accessed via the ||| operator.

Each bit of the resulting integer is set if at least one of the corresponding bits of the input integers is set, according to the two's complement representation.

This function is overridden at runtime with an efficient implementation.

Equations

• a.lor b = { toUInt32 := { toBitVec := a.toBitVec ||| b.toBitVec } }

@[extern lean_int32_xor]

def Int32.xor (a b : Int32) : Int32

Bitwise exclusive or for 32-bit signed integers. Usually accessed via the ^^^ operator.

Each bit of the resulting integer is set if exactly one of the corresponding bits of the input integers is set, according to the two's complement representation.

This function is overridden at runtime with an efficient implementation.

Equations

• a.xor b = { toUInt32 := { toBitVec := a.toBitVec ^^^ b.toBitVec } }

@[extern lean_int32_shift_left]

def Int32.shiftLeft (a b : Int32) : Int32

Bitwise left shift for 32-bit signed integers. Usually accessed via the <<< operator.

Signed integers are interpreted as bitvectors according to the two's complement representation.

This function is overridden at runtime with an efficient implementation.

Equations

• a.shiftLeft b = { toUInt32 := { toBitVec := a.toBitVec <<< b.toBitVec.smod 32 } }

@[extern lean_int32_shift_right]

def Int32.shiftRight (a b : Int32) : Int32

Arithmetic right shift for 32-bit signed integers. Usually accessed via the <<< operator.

The high bits are filled with the value of the most significant bit.

This function is overridden at runtime with an efficient implementation.

Equations

• a.shiftRight b = { toUInt32 := { toBitVec := a.toBitVec.sshiftRight' (b.toBitVec.smod 32) } }

@[extern lean_int32_complement]

def Int32.complement (a : Int32) : Int32

Bitwise complement, also known as bitwise negation, for 32-bit signed integers. Usually accessed via the ~~~ prefix operator.

Each bit of the resulting integer is the opposite of the corresponding bit of the input integer. Integers use the two's complement representation, so Int32.complement a = -(a + 1).

This function is overridden at runtime with an efficient implementation.

Equations

• a.complement = { toUInt32 := { toBitVec := ~~~a.toBitVec } }

@[extern lean_int32_abs]

def Int32.abs (a : Int32) : Int32

Computes the absolute value of a 32-bit signed integer.

This function is equivalent to if a < 0 then -a else a, so in particular Int32.minValue will be mapped to Int32.minValue.

This function is overridden at runtime with an efficient implementation.

Equations

• a.abs = { toUInt32 := { toBitVec := a.toBitVec.abs } }

@[extern lean_int32_dec_eq]

def Int32.decEq (a b : Int32) : Decidable (a = b)

Decides whether two 32-bit signed integers are equal. Usually accessed via the DecidableEq Int32 instance.

This function is overridden at runtime with an efficient implementation.

Examples:

• Int32.decEq 123 123 = .isTrue rfl
• (if ((-7) : Int32) = 7 then "yes" else "no") = "no"
• show (7 : Int32) = 7 by decide

Equations

• { toUInt32 := n }.decEq { toUInt32 := m } = if h : n = m then isTrue ⋯ else isFalse ⋯

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

Strict inequality of 32-bit signed integers, defined as inequality of the corresponding integers. Usually accessed via the < operator.

Equations

• a.lt b = (a.toBitVec.slt b.toBitVec = true)

def Int32.le (a b : Int32) : Prop

Non-strict inequality of 32-bit signed integers, defined as inequality of the corresponding integers. Usually accessed via the ≤ operator.

Equations

• a.le b = (a.toBitVec.sle b.toBitVec = true)

instance instInhabitedInt32 : Inhabited Int32

Equations

• instInhabitedInt32 = { default := 0 }

instance instAddInt32 : Add Int32

Equations

• instAddInt32 = { add := Int32.add }

instance instSubInt32 : Sub Int32

Equations

• instSubInt32 = { sub := Int32.sub }

instance instMulInt32 : Mul Int32

Equations

• instMulInt32 = { mul := Int32.mul }

instance instModInt32 : Mod Int32

Equations

• instModInt32 = { mod := Int32.mod }

instance instDivInt32 : Div Int32

Equations

• instDivInt32 = { div := Int32.div }

instance instLTInt32 : LT Int32

Equations

• instLTInt32 = { lt := Int32.lt }

instance instLEInt32 : LE Int32

Equations

• instLEInt32 = { le := Int32.le }

instance instComplementInt32 : Complement Int32

Equations

• instComplementInt32 = { complement := Int32.complement }

instance instAndOpInt32 : AndOp Int32

Equations

• instAndOpInt32 = { and := Int32.land }

instance instOrOpInt32 : OrOp Int32

Equations

• instOrOpInt32 = { or := Int32.lor }

instance instXorInt32 : Xor Int32

Equations

• instXorInt32 = { xor := Int32.xor }

instance instShiftLeftInt32 : ShiftLeft Int32

Equations

• instShiftLeftInt32 = { shiftLeft := Int32.shiftLeft }

instance instShiftRightInt32 : ShiftRight Int32

Equations

• instShiftRightInt32 = { shiftRight := Int32.shiftRight }

instance instDecidableEqInt32 : DecidableEq Int32

Equations

• instDecidableEqInt32 = Int32.decEq

@[extern lean_bool_to_int32]

def Bool.toInt32 (b : Bool) : Int32

Converts true to 1 and false to 0.

Equations

• b.toInt32 = if b = true then 1 else 0

@[extern lean_int32_dec_lt]

def Int32.decLt (a b : Int32) : Decidable (a < b)

Decides whether one 32-bit signed integer is strictly less than another. Usually accessed via the DecidableLT Int32 instance.

This function is overridden at runtime with an efficient implementation.

Examples:

• (if ((-7) : Int32) < 7 then "yes" else "no") = "yes"
• (if (5 : Int32) < 5 then "yes" else "no") = "no"
• show ¬((7 : Int32) < 7) by decide

Equations

• a.decLt b = inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec = true))

@[extern lean_int32_dec_le]

def Int32.decLe (a b : Int32) : Decidable (a ≤ b)

Decides whether one 32-bit signed integer is less than or equal to another. Usually accessed via the DecidableLE Int32 instance.

This function is overridden at runtime with an efficient implementation.

Examples:

• (if ((-7) : Int32) ≤ 7 then "yes" else "no") = "yes"
• (if (15 : Int32) ≤ 15 then "yes" else "no") = "yes"
• (if (15 : Int32) ≤ 5 then "yes" else "no") = "no"
• show (7 : Int32) ≤ 7 by decide

Equations

• a.decLe b = inferInstanceAs (Decidable (a.toBitVec.sle b.toBitVec = true))

instance instDecidableLtInt32 (a b : Int32) : Decidable (a < b)

Equations

• instDecidableLtInt32 a b = a.decLt b

instance instDecidableLeInt32 (a b : Int32) : Decidable (a ≤ b)

Equations

• instDecidableLeInt32 a b = a.decLe b

instance instMaxInt32 : Max Int32

Equations

• instMaxInt32 = maxOfLe

instance instMinInt32 : Min Int32

Equations

• instMinInt32 = minOfLe

@[reducible, inline]

abbrev Int64.size : Nat

The number of distinct values representable by Int64, that is, 2^64 = 18446744073709551616.

Equations

• Int64.size = 18446744073709551616

@[inline]

def Int64.toBitVec (x : Int64) : BitVec 64

Obtain the BitVec that contains the 2's complement representation of the Int64.

Equations

• x.toBitVec = x.toUInt64.toBitVec

theorem Int64.toBitVec.inj {x y : Int64} : x.toBitVec = y.toBitVec → x = y

@[inline]

def UInt64.toInt64 (i : UInt64) : Int64

Obtains the Int64 that is 2's complement equivalent to the UInt64.

Equations

• i.toInt64 = { toUInt64 := i }

@[inline, deprecated UInt64.toInt64 (since := "2025-02-13")]

def Int64.mk (i : UInt64) : Int64

Obtains the Int64 that is 2's complement equivalent to the UInt64.

Equations

• Int64.mk i = i.toInt64

@[extern lean_int64_of_int]

def Int64.ofInt (i : Int) : Int64

Converts an arbitrary-precision integer to a 64-bit integer, wrapping on overflow or underflow.

This function is overridden at runtime with an efficient implementation.

Examples:

• Int64.ofInt 48 = 48
• Int64.ofInt (-40_000) = -40_000
• Int64.ofInt 2_147_483_648 = 2_147_483_648
• Int64.ofInt (-2_147_483_649) = -2_147_483_649
• Int64.ofInt 9_223_372_036_854_775_808 = -9_223_372_036_854_775_808
• Int64.ofInt (-9_223_372_036_854_775_809) = 9_223_372_036_854_775_807

Equations

• Int64.ofInt i = { toUInt64 := { toBitVec := BitVec.ofInt 64 i } }

@[extern lean_int64_of_nat]

def Int64.ofNat (n : Nat) : Int64

Converts a natural number to a 64-bit signed integer, wrapping around to negative numbers on overflow.

This function is overridden at runtime with an efficient implementation.

Examples:

• Int64.ofNat 127 = 127
• Int64.ofNat 2_147_483_648 = 2_147_483_648
• Int64.ofNat 9_223_372_036_854_775_807 = 9_223_372_036_854_775_807
• Int64.ofNat 9_223_372_036_854_775_808 = -9_223_372_036_854_775_808
• Int64.ofNat 18_446_744_073_709_551_618 = 0

Equations

• Int64.ofNat n = { toUInt64 := { toBitVec := BitVec.ofNat 64 n } }

@[reducible, inline]

abbrev Int.toInt64 (i : Int) : Int64

Converts an arbitrary-precision integer to a 64-bit integer, wrapping on overflow or underflow.

This function is overridden at runtime with an efficient implementation.

Examples:

• Int.toInt64 48 = 48
• Int.toInt64 (-40_000) = -40_000
• Int.toInt64 2_147_483_648 = 2_147_483_648
• Int.toInt64 (-2_147_483_649) = -2_147_483_649
• Int.toInt64 9_223_372_036_854_775_808 = -9_223_372_036_854_775_808
• Int.toInt64 (-9_223_372_036_854_775_809) = 9_223_372_036_854_775_807

Equations

• Int.toInt64 = Int64.ofInt

@[reducible, inline]

abbrev Nat.toInt64 (n : Nat) : Int64

Converts a natural number to a 64-bit signed integer, wrapping around to negative numbers on overflow.

Examples:

• Nat.toInt64 127 = 127
• Nat.toInt64 2_147_483_648 = 2_147_483_648
• Nat.toInt64 9_223_372_036_854_775_807 = 9_223_372_036_854_775_807
• Nat.toInt64 9_223_372_036_854_775_808 = -9_223_372_036_854_775_808
• Nat.toInt64 18_446_744_073_709_551_618 = 0

Equations

• Nat.toInt64 = Int64.ofNat

@[extern lean_int64_to_int_sint]

def Int64.toInt (i : Int64) : Int

Converts a 64-bit signed integer to an arbitrary-precision integer that denotes the same number.

This function is overridden at runtime with an efficient implementation.

Equations

• i.toInt = i.toBitVec.toInt

@[inline]

def Int64.toNatClampNeg (i : Int64) : Nat

Converts a 64-bit signed integer to a natural number, mapping all negative numbers to 0.

Use Int64.toBitVec to obtain the two's complement representation.

Equations

• i.toNatClampNeg = i.toInt.toNat

@[inline, deprecated Int64.toNatClampNeg (since := "2025-02-13")]

def Int64.toNat (i : Int64) : Nat

Converts a 64-bit signed integer to a natural number, mapping all negative numbers to 0.

Use Int64.toBitVec to obtain the two's complement representation.

Equations

• i.toNat = i.toInt.toNat

@[inline]

def Int64.ofBitVec (b : BitVec 64) : Int64

Obtains the Int64 whose 2's complement representation is the given BitVec 64.

Equations

• Int64.ofBitVec b = { toUInt64 := { toBitVec := b } }

@[extern lean_int64_to_int8]

def Int64.toInt8 (a : Int64) : Int8

Converts a 64-bit signed integer to an 8-bit signed integer by truncating its bitvector representation.

This function is overridden at runtime with an efficient implementation.

Equations

• a.toInt8 = { toUInt8 := { toBitVec := BitVec.signExtend 8 a.toBitVec } }

@[extern lean_int64_to_int16]

def Int64.toInt16 (a : Int64) : Int16

Converts a 64-bit signed integer to a 16-bit signed integer by truncating its bitvector representation.

This function is overridden at runtime with an efficient implementation.

Equations

• a.toInt16 = { toUInt16 := { toBitVec := BitVec.signExtend 16 a.toBitVec } }

@[extern lean_int64_to_int32]

def Int64.toInt32 (a : Int64) : Int32

Converts a 64-bit signed integer to a 32-bit signed integer by truncating its bitvector representation.

This function is overridden at runtime with an efficient implementation.

Equations

• a.toInt32 = { toUInt32 := { toBitVec := BitVec.signExtend 32 a.toBitVec } }

@[extern lean_int8_to_int64]

def Int8.toInt64 (a : Int8) : Int64

Converts 8-bit signed integers to 64-bit signed integers that denote the same number.

This function is overridden at runtime with an efficient implementation.

Equations

• a.toInt64 = { toUInt64 := { toBitVec := BitVec.signExtend 64 a.toBitVec } }

@[extern lean_int16_to_int64]

def Int16.toInt64 (a : Int16) : Int64

Converts 16-bit signed integers to 64-bit signed integers that denote the same number.

This function is overridden at runtime with an efficient implementation.

Equations

• a.toInt64 = { toUInt64 := { toBitVec := BitVec.signExtend 64 a.toBitVec } }

@[extern lean_int32_to_int64]

def Int32.toInt64 (a : Int32) : Int64

Converts 32-bit signed integers to 64-bit signed integers that denote the same number.

This function is overridden at runtime with an efficient implementation.

Equations

• a.toInt64 = { toUInt64 := { toBitVec := BitVec.signExtend 64 a.toBitVec } }

@[extern lean_int64_neg]

def Int64.neg (i : Int64) : Int64

Negates 64-bit signed integers. Usually accessed via the - prefix operator.

This function is overridden at runtime with an efficient implementation.

Equations

• i.neg = { toUInt64 := { toBitVec := -i.toBitVec } }

instance instToStringInt64 : ToString Int64

Equations

• instToStringInt64 = { toString := fun (i : Int64) => toString i.toInt }

instance instReprInt64 : Repr Int64

Equations

• instReprInt64 = { reprPrec := fun (i : Int64) (prec : Nat) => reprPrec i.toInt prec }

instance instReprAtomInt64 : ReprAtom Int64

Equations

• instReprAtomInt64 = { }

instance instHashableInt64 : Hashable Int64

Equations

• instHashableInt64 = { hash := fun (i : Int64) => i.toUInt64 }

instance Int64.instOfNat {n : Nat} : OfNat Int64 n

Equations

• Int64.instOfNat = { ofNat := Int64.ofNat n }

instance Int64.instNeg : Neg Int64

Equations

• Int64.instNeg = { neg := Int64.neg }

@[reducible, inline]

abbrev Int64.maxValue : Int64

The largest number that Int64 can represent: 2^63 - 1 = 9223372036854775807.

Equations

• Int64.maxValue = 9223372036854775807

@[reducible, inline]

abbrev Int64.minValue : Int64

The smallest number that Int64 can represent: -2^63 = -9223372036854775808.

Equations

• Int64.minValue = -9223372036854775808

@[inline]

def Int64.ofIntLE (i : Int) (_hl : minValue.toInt ≤ i) (_hr : i ≤ maxValue.toInt) : Int64

Constructs an Int64 from an Int that is known to be in bounds.

Equations

• Int64.ofIntLE i _hl _hr = Int64.ofInt i

def Int64.ofIntTruncate (i : Int) : Int64

Constructs an Int64 from an Int, clamping if the value is too small or too large.

Equations

• Int64.ofIntTruncate i = if hl : Int64.minValue.toInt ≤ i then if hr : i ≤ Int64.maxValue.toInt then Int64.ofIntLE i hl hr else Int64.minValue else Int64.minValue

@[extern lean_int64_add]

def Int64.add (a b : Int64) : Int64

Adds two 64-bit signed integers, wrapping around on over- or underflow. Usually accessed via the + operator.

This function is overridden at runtime with an efficient implementation.

Equations

• a.add b = { toUInt64 := { toBitVec := a.toBitVec + b.toBitVec } }

@[extern lean_int64_sub]

def Int64.sub (a b : Int64) : Int64

Subtracts one 64-bit signed integer from another, wrapping around on over- or underflow. Usually accessed via the - operator.

This function is overridden at runtime with an efficient implementation.

Equations

• a.sub b = { toUInt64 := { toBitVec := a.toBitVec - b.toBitVec } }

@[extern lean_int64_mul]

def Int64.mul (a b : Int64) : Int64

Multiplies two 64-bit signed integers, wrapping around on over- or underflow. Usually accessed via the * operator.

This function is overridden at runtime with an efficient implementation.

Equations

• a.mul b = { toUInt64 := { toBitVec := a.toBitVec * b.toBitVec } }

@[extern lean_int64_div]

def Int64.div (a b : Int64) : Int64

Truncating division for 64-bit signed integers, rounding towards zero. Usually accessed via the / operator.

Division by zero is defined to be zero.

This function is overridden at runtime with an efficient implementation.

Examples:

• Int64.div 10 3 = 3
• Int64.div 10 (-3) = (-3)
• Int64.div (-10) (-3) = 3
• Int64.div (-10) 3 = (-3)
• Int64.div 10 0 = 0

Equations

• a.div b = { toUInt64 := { toBitVec := a.toBitVec.sdiv b.toBitVec } }

@[extern lean_int64_mod]

def Int64.mod (a b : Int64) : Int64

The modulo operator for 64-bit signed integers, which computes the remainder when dividing one integer by another with the T-rounding convention used by Int64.div. Usually accessed via the % operator.

When the divisor is 0, the result is the dividend rather than an error.

This function is overridden at runtime with an efficient implementation.

Examples:

• Int64.mod 5 2 = 1
• Int64.mod 5 (-2) = 1
• Int64.mod (-5) 2 = (-1)
• Int64.mod (-5) (-2) = (-1)
• Int64.mod 4 2 = 0
• Int64.mod 4 (-2) = 0
• Int64.mod 4 0 = 4
• Int64.mod (-4) 0 = (-4)

Equations

• a.mod b = { toUInt64 := { toBitVec := a.toBitVec.srem b.toBitVec } }

@[extern lean_int64_land]

def Int64.land (a b : Int64) : Int64

Bitwise and for 64-bit signed integers. Usually accessed via the &&& operator.

Each bit of the resulting integer is set if the corresponding bits of both input integers are set, according to the two's complement representation.

This function is overridden at runtime with an efficient implementation.

Equations

• a.land b = { toUInt64 := { toBitVec := a.toBitVec &&& b.toBitVec } }

@[extern lean_int64_lor]

def Int64.lor (a b : Int64) : Int64

Bitwise or for 64-bit signed integers. Usually accessed via the ||| operator.

Each bit of the resulting integer is set if at least one of the corresponding bits of the input integers is set, according to the two's complement representation.

This function is overridden at runtime with an efficient implementation.

Equations

• a.lor b = { toUInt64 := { toBitVec := a.toBitVec ||| b.toBitVec } }

@[extern lean_int64_xor]

def Int64.xor (a b : Int64) : Int64

Bitwise exclusive or for 64-bit signed integers. Usually accessed via the ^^^ operator.

Each bit of the resulting integer is set if exactly one of the corresponding bits of the input integers is set, according to the two's complement representation.

This function is overridden at runtime with an efficient implementation.

Equations

• a.xor b = { toUInt64 := { toBitVec := a.toBitVec ^^^ b.toBitVec } }

@[extern lean_int64_shift_left]

def Int64.shiftLeft (a b : Int64) : Int64

Bitwise left shift for 64-bit signed integers. Usually accessed via the <<< operator.

Signed integers are interpreted as bitvectors according to the two's complement representation.

This function is overridden at runtime with an efficient implementation.

Equations

• a.shiftLeft b = { toUInt64 := { toBitVec := a.toBitVec <<< b.toBitVec.smod 64 } }

@[extern lean_int64_shift_right]

def Int64.shiftRight (a b : Int64) : Int64

Arithmetic right shift for 64-bit signed integers. Usually accessed via the <<< operator.

The high bits are filled with the value of the most significant bit.

This function is overridden at runtime with an efficient implementation.

Equations

• a.shiftRight b = { toUInt64 := { toBitVec := a.toBitVec.sshiftRight' (b.toBitVec.smod 64) } }

@[extern lean_int64_complement]

def Int64.complement (a : Int64) : Int64

Bitwise complement, also known as bitwise negation, for 64-bit signed integers. Usually accessed via the ~~~ prefix operator.

Each bit of the resulting integer is the opposite of the corresponding bit of the input integer. Integers use the two's complement representation, so Int64.complement a = -(a + 1).

This function is overridden at runtime with an efficient implementation.

Equations

• a.complement = { toUInt64 := { toBitVec := ~~~a.toBitVec } }

@[extern lean_int64_abs]

def Int64.abs (a : Int64) : Int64

Computes the absolute value of a 64-bit signed integer.

This function is equivalent to if a < 0 then -a else a, so in particular Int64.minValue will be mapped to Int64.minValue.

This function is overridden at runtime with an efficient implementation.

Equations

• a.abs = { toUInt64 := { toBitVec := a.toBitVec.abs } }

@[extern lean_int64_dec_eq]

def Int64.decEq (a b : Int64) : Decidable (a = b)

Decides whether two 64-bit signed integers are equal. Usually accessed via the DecidableEq Int64 instance.

This function is overridden at runtime with an efficient implementation.

Examples:

• Int64.decEq 123 123 = .isTrue rfl
• (if ((-7) : Int64) = 7 then "yes" else "no") = "no"
• show (7 : Int64) = 7 by decide

Equations

• { toUInt64 := n }.decEq { toUInt64 := m } = if h : n = m then isTrue ⋯ else isFalse ⋯

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

Strict inequality of 64-bit signed integers, defined as inequality of the corresponding integers. Usually accessed via the < operator.

Equations

• a.lt b = (a.toBitVec.slt b.toBitVec = true)

def Int64.le (a b : Int64) : Prop

Non-strict inequality of 64-bit signed integers, defined as inequality of the corresponding integers. Usually accessed via the ≤ operator.

Equations

• a.le b = (a.toBitVec.sle b.toBitVec = true)

instance instInhabitedInt64 : Inhabited Int64

Equations

• instInhabitedInt64 = { default := 0 }

instance instAddInt64 : Add Int64

Equations

• instAddInt64 = { add := Int64.add }

instance instSubInt64 : Sub Int64

Equations

• instSubInt64 = { sub := Int64.sub }

instance instMulInt64 : Mul Int64

Equations

• instMulInt64 = { mul := Int64.mul }

instance instModInt64 : Mod Int64

Equations

• instModInt64 = { mod := Int64.mod }

instance instDivInt64 : Div Int64

Equations

• instDivInt64 = { div := Int64.div }

instance instLTInt64 : LT Int64

Equations

• instLTInt64 = { lt := Int64.lt }

instance instLEInt64 : LE Int64

Equations

• instLEInt64 = { le := Int64.le }

instance instComplementInt64 : Complement Int64

Equations

• instComplementInt64 = { complement := Int64.complement }

instance instAndOpInt64 : AndOp Int64

Equations

• instAndOpInt64 = { and := Int64.land }

instance instOrOpInt64 : OrOp Int64

Equations

• instOrOpInt64 = { or := Int64.lor }

instance instXorInt64 : Xor Int64

Equations

• instXorInt64 = { xor := Int64.xor }

instance instShiftLeftInt64 : ShiftLeft Int64

Equations

• instShiftLeftInt64 = { shiftLeft := Int64.shiftLeft }

instance instShiftRightInt64 : ShiftRight Int64

Equations

• instShiftRightInt64 = { shiftRight := Int64.shiftRight }

instance instDecidableEqInt64 : DecidableEq Int64

Equations

• instDecidableEqInt64 = Int64.decEq

@[extern lean_bool_to_int64]

def Bool.toInt64 (b : Bool) : Int64

Converts true to 1 and false to 0.

Equations

• b.toInt64 = if b = true then 1 else 0

@[extern lean_int64_dec_lt]

def Int64.decLt (a b : Int64) : Decidable (a < b)

Decides whether one 8-bit signed integer is strictly less than another. Usually accessed via the DecidableLT Int64 instance.

This function is overridden at runtime with an efficient implementation.

Examples:

• (if ((-7) : Int64) < 7 then "yes" else "no") = "yes"
• (if (5 : Int64) < 5 then "yes" else "no") = "no"
• show ¬((7 : Int64) < 7) by decide

Equations

• a.decLt b = inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec = true))

@[extern lean_int64_dec_le]

def Int64.decLe (a b : Int64) : Decidable (a ≤ b)

Decides whether one 8-bit signed integer is less than or equal to another. Usually accessed via the DecidableLE Int64 instance.

This function is overridden at runtime with an efficient implementation.

Examples:

• (if ((-7) : Int64) ≤ 7 then "yes" else "no") = "yes"
• (if (15 : Int64) ≤ 15 then "yes" else "no") = "yes"
• (if (15 : Int64) ≤ 5 then "yes" else "no") = "no"
• show (7 : Int64) ≤ 7 by decide

Equations

• a.decLe b = inferInstanceAs (Decidable (a.toBitVec.sle b.toBitVec = true))

instance instDecidableLtInt64 (a b : Int64) : Decidable (a < b)

Equations

• instDecidableLtInt64 a b = a.decLt b

instance instDecidableLeInt64 (a b : Int64) : Decidable (a ≤ b)

Equations

• instDecidableLeInt64 a b = a.decLe b

instance instMaxInt64 : Max Int64

Equations

• instMaxInt64 = maxOfLe

instance instMinInt64 : Min Int64

Equations

• instMinInt64 = minOfLe

@[reducible, inline]

abbrev ISize.size : Nat

The number of distinct values representable by ISize, that is, 2^System.Platform.numBits.

Equations

• ISize.size = 2 ^ System.Platform.numBits

@[inline]

def ISize.toBitVec (x : ISize) : BitVec System.Platform.numBits

Obtain the BitVec that contains the 2's complement representation of the ISize.

Equations

• x.toBitVec = x.toUSize.toBitVec

theorem ISize.toBitVec.inj {x y : ISize} : x.toBitVec = y.toBitVec → x = y

@[inline]

def USize.toISize (i : USize) : ISize

Obtains the ISize that is 2's complement equivalent to the USize.

Equations

• i.toISize = { toUSize := i }

@[inline, deprecated USize.toISize (since := "2025-02-13")]

def ISize.mk (i : USize) : ISize

Obtains the ISize that is 2's complement equivalent to the USize.

Equations

• ISize.mk i = i.toISize

@[extern lean_isize_of_int]

def ISize.ofInt (i : Int) : ISize

Converts an arbitrary-precision integer to a word-sized signed integer, wrapping around on over- or underflow.

This function is overridden at runtime with an efficient implementation.

Equations

• ISize.ofInt i = { toUSize := { toBitVec := BitVec.ofInt System.Platform.numBits i } }

@[extern lean_isize_of_nat]

def ISize.ofNat (n : Nat) : ISize

Converts an arbitrary-precision natural number to a word-sized signed integer, wrapping around on overflow.

This function is overridden at runtime with an efficient implementation.

Equations

• ISize.ofNat n = { toUSize := { toBitVec := BitVec.ofNat System.Platform.numBits n } }

@[reducible, inline]

abbrev Int.toISize (i : Int) : ISize

Converts an arbitrary-precision integer to a word-sized signed integer, wrapping around on over- or underflow.

This function is overridden at runtime with an efficient implementation.

Equations

• Int.toISize = ISize.ofInt

@[reducible, inline]

abbrev Nat.toISize (n : Nat) : ISize

Converts an arbitrary-precision natural number to a word-sized signed integer, wrapping around on overflow.

This function is overridden at runtime with an efficient implementation.

Equations

• Nat.toISize = ISize.ofNat

@[extern lean_isize_to_int]

def ISize.toInt (i : ISize) : Int

Converts a word-sized signed integer to an arbitrary-precision integer that denotes the same number.

This function is overridden at runtime with an efficient implementation.

Equations

• i.toInt = i.toBitVec.toInt

@[inline]

def ISize.toNatClampNeg (i : ISize) : Nat

Converts a word-sized signed integer to a natural number, mapping all negative numbers to 0.

Use ISize.toBitVec to obtain the two's complement representation.

Equations

• i.toNatClampNeg = i.toInt.toNat

@[inline, deprecated ISize.toNatClampNeg (since := "2025-02-13")]

def ISize.toNat (i : ISize) : Nat

Converts a word-sized signed integer to a natural number, mapping all negative numbers to 0.

Use ISize.toBitVec to obtain the two's complement representation.

Equations

• i.toNat = i.toInt.toNat

@[inline]

def ISize.ofBitVec (b : BitVec System.Platform.numBits) : ISize

Obtains the ISize whose 2's complement representation is the given BitVec.

Equations

• ISize.ofBitVec b = { toUSize := { toBitVec := b } }

@[extern lean_isize_to_int8]

def ISize.toInt8 (a : ISize) : Int8

Converts a word-sized signed integer to an 8-bit signed integer by truncating its bitvector representation.

This function is overridden at runtime with an efficient implementation.

Equations

• a.toInt8 = { toUInt8 := { toBitVec := BitVec.signExtend 8 a.toBitVec } }

@[extern lean_isize_to_int16]

def ISize.toInt16 (a : ISize) : Int16

Converts a word-sized integer to a 16-bit integer by truncating its bitvector representation.

This function is overridden at runtime with an efficient implementation.

Equations

• a.toInt16 = { toUInt16 := { toBitVec := BitVec.signExtend 16 a.toBitVec } }

@[extern lean_isize_to_int32]

def ISize.toInt32 (a : ISize) : Int32

Converts a word-sized signed integer to a 32-bit signed integer.

On 32-bit platforms, this conversion is lossless. On 64-bit platforms, the integer's bitvector representation is truncated to 32 bits. This function is overridden at runtime with an efficient implementation.

This function is overridden at runtime with an efficient implementation.

Equations

• a.toInt32 = { toUInt32 := { toBitVec := BitVec.signExtend 32 a.toBitVec } }

@[extern lean_isize_to_int64]

def ISize.toInt64 (a : ISize) : Int64

Converts word-sized signed integers to 64-bit signed integers that denote the same number. This conversion is lossless, because ISize is either Int32 or Int64.

This function is overridden at runtime with an efficient implementation.

Equations

• a.toInt64 = { toUInt64 := { toBitVec := BitVec.signExtend 64 a.toBitVec } }

@[extern lean_int8_to_isize]

def Int8.toISize (a : Int8) : ISize

Converts 8-bit signed integers to word-sized signed integers that denote the same number. This conversion is lossless, because ISize is either Int32 or Int64.

This function is overridden at runtime with an efficient implementation.

Equations

• a.toISize = { toUSize := { toBitVec := BitVec.signExtend System.Platform.numBits a.toBitVec } }

@[extern lean_int16_to_isize]

def Int16.toISize (a : Int16) : ISize

Converts 16-bit signed integers to word-sized signed integers that denote the same number. This conversion is lossless, because ISize is either Int32 or Int64.

This function is overridden at runtime with an efficient implementation.

Equations

• a.toISize = { toUSize := { toBitVec := BitVec.signExtend System.Platform.numBits a.toBitVec } }

@[extern lean_int32_to_isize]

def Int32.toISize (a : Int32) : ISize

Converts 32-bit signed integers to word-sized signed integers that denote the same number. This conversion is lossless, because ISize is either Int32 or Int64.

This function is overridden at runtime with an efficient implementation.

Equations

• a.toISize = { toUSize := { toBitVec := BitVec.signExtend System.Platform.numBits a.toBitVec } }

@[extern lean_int64_to_isize]

def Int64.toISize (a : Int64) : ISize

Converts 64-bit signed integers to word-sized signed integers, truncating the bitvector representation on 32-bit platforms. This conversion is lossless on 64-bit platforms.

This function is overridden at runtime with an efficient implementation.

Equations

• a.toISize = { toUSize := { toBitVec := BitVec.signExtend System.Platform.numBits a.toBitVec } }

@[extern lean_isize_neg]

def ISize.neg (i : ISize) : ISize

Negates word-sized signed integers. Usually accessed via the - prefix operator.

This function is overridden at runtime with an efficient implementation.

Equations

• i.neg = { toUSize := { toBitVec := -i.toBitVec } }

instance instToStringISize : ToString ISize

Equations

• instToStringISize = { toString := fun (i : ISize) => toString i.toInt }

instance instReprISize : Repr ISize

Equations

• instReprISize = { reprPrec := fun (i : ISize) (prec : Nat) => reprPrec i.toInt prec }

instance instReprAtomISize : ReprAtom ISize

Equations

• instReprAtomISize = { }

instance instHashableISize : Hashable ISize

Equations

• instHashableISize = { hash := fun (i : ISize) => i.toUSize.toUInt64 }

instance ISize.instOfNat {n : Nat} : OfNat ISize n

Equations

• ISize.instOfNat = { ofNat := ISize.ofNat n }

instance ISize.instNeg : Neg ISize

Equations

• ISize.instNeg = { neg := ISize.neg }

@[reducible, inline]

abbrev ISize.maxValue : ISize

The largest number that ISize can represent: 2^(System.Platform.numBits - 1) - 1.

Equations

• ISize.maxValue = ISize.ofInt (2 ^ (System.Platform.numBits - 1) - 1)

@[reducible, inline]

abbrev ISize.minValue : ISize

The smallest number that ISize can represent: -2^(System.Platform.numBits - 1).

Equations

• ISize.minValue = ISize.ofInt (-2 ^ (System.Platform.numBits - 1))

@[inline]

def ISize.ofIntLE (i : Int) (_hl : minValue.toInt ≤ i) (_hr : i ≤ maxValue.toInt) : ISize

Constructs an ISize from an Int that is known to be in bounds.

Equations

• ISize.ofIntLE i _hl _hr = ISize.ofInt i

def ISize.ofIntTruncate (i : Int) : ISize

Constructs an ISize from an Int, clamping if the value is too small or too large.

Equations

• ISize.ofIntTruncate i = if hl : ISize.minValue.toInt ≤ i then if hr : i ≤ ISize.maxValue.toInt then ISize.ofIntLE i hl hr else ISize.minValue else ISize.minValue

@[extern lean_isize_add]

def ISize.add (a b : ISize) : ISize

Adds two word-sized signed integers, wrapping around on over- or underflow. Usually accessed via the + operator.

This function is overridden at runtime with an efficient implementation.

Equations

• a.add b = { toUSize := { toBitVec := a.toBitVec + b.toBitVec } }

@[extern lean_isize_sub]

def ISize.sub (a b : ISize) : ISize

Subtracts one word-sized signed integer from another, wrapping around on over- or underflow. Usually accessed via the - operator.

This function is overridden at runtime with an efficient implementation.

Equations

• a.sub b = { toUSize := { toBitVec := a.toBitVec - b.toBitVec } }

@[extern lean_isize_mul]

def ISize.mul (a b : ISize) : ISize

Multiplies two word-sized signed integers, wrapping around on over- or underflow. Usually accessed via the * operator.

This function is overridden at runtime with an efficient implementation.

Equations

• a.mul b = { toUSize := { toBitVec := a.toBitVec * b.toBitVec } }

@[extern lean_isize_div]

def ISize.div (a b : ISize) : ISize

Truncating division for word-sized signed integers, rounding towards zero. Usually accessed via the / operator.

Division by zero is defined to be zero.

This function is overridden at runtime with an efficient implementation.

Examples:

• ISize.div 10 3 = 3
• ISize.div 10 (-3) = (-3)
• ISize.div (-10) (-3) = 3
• ISize.div (-10) 3 = (-3)
• ISize.div 10 0 = 0

Equations

• a.div b = { toUSize := { toBitVec := a.toBitVec.sdiv b.toBitVec } }

@[extern lean_isize_mod]

def ISize.mod (a b : ISize) : ISize

The modulo operator for word-sized signed integers, which computes the remainder when dividing one integer by another with the T-rounding convention used by ISize.div. Usually accessed via the % operator.

When the divisor is 0, the result is the dividend rather than an error.

This function is overridden at runtime with an efficient implementation.

Examples:

• ISize.mod 5 2 = 1
• ISize.mod 5 (-2) = 1
• ISize.mod (-5) 2 = (-1)
• ISize.mod (-5) (-2) = (-1)
• ISize.mod 4 2 = 0
• ISize.mod 4 (-2) = 0
• ISize.mod 4 0 = 4
• ISize.mod (-4) 0 = (-4)

Equations

• a.mod b = { toUSize := { toBitVec := a.toBitVec.srem b.toBitVec } }

@[extern lean_isize_land]

def ISize.land (a b : ISize) : ISize

Bitwise and for word-sized signed integers. Usually accessed via the &&& operator.

Each bit of the resulting integer is set if the corresponding bits of both input integers are set, according to the two's complement representation.

This function is overridden at runtime with an efficient implementation.

Equations

• a.land b = { toUSize := { toBitVec := a.toBitVec &&& b.toBitVec } }

@[extern lean_isize_lor]

def ISize.lor (a b : ISize) : ISize

Bitwise or for word-sized signed integers. Usually accessed via the ||| operator.

Each bit of the resulting integer is set if at least one of the corresponding bits of the input integers is set, according to the two's complement representation.

This function is overridden at runtime with an efficient implementation.

Equations

• a.lor b = { toUSize := { toBitVec := a.toBitVec ||| b.toBitVec } }

@[extern lean_isize_xor]

def ISize.xor (a b : ISize) : ISize

Bitwise exclusive or for word-sized signed integers. Usually accessed via the ^^^ operator.

Each bit of the resulting integer is set if exactly one of the corresponding bits of the input integers is set, according to the two's complement representation.

This function is overridden at runtime with an efficient implementation.

Equations

• a.xor b = { toUSize := { toBitVec := a.toBitVec ^^^ b.toBitVec } }

@[extern lean_isize_shift_left]

def ISize.shiftLeft (a b : ISize) : ISize

Bitwise left shift for word-sized signed integers. Usually accessed via the <<< operator.

Signed integers are interpreted as bitvectors according to the two's complement representation.

This function is overridden at runtime with an efficient implementation.

Equations

• a.shiftLeft b = { toUSize := { toBitVec := a.toBitVec <<< b.toBitVec.smod ↑System.Platform.numBits } }

@[extern lean_isize_shift_right]

def ISize.shiftRight (a b : ISize) : ISize

Arithmetic right shift for word-sized signed integers. Usually accessed via the <<< operator.

The high bits are filled with the value of the most significant bit.

This function is overridden at runtime with an efficient implementation.

Equations

• a.shiftRight b = { toUSize := { toBitVec := a.toBitVec.sshiftRight' (b.toBitVec.smod ↑System.Platform.numBits) } }

@[extern lean_isize_complement]

def ISize.complement (a : ISize) : ISize

Bitwise complement, also known as bitwise negation, for word-sized signed integers. Usually accessed via the ~~~ prefix operator.

Each bit of the resulting integer is the opposite of the corresponding bit of the input integer. Integers use the two's complement representation, so ISize.complement a = -(a + 1).

This function is overridden at runtime with an efficient implementation.

Equations

• a.complement = { toUSize := { toBitVec := ~~~a.toBitVec } }

@[extern lean_isize_abs]

def ISize.abs (a : ISize) : ISize

Computes the absolute value of a word-sized signed integer.

This function is equivalent to if a < 0 then -a else a, so in particular ISize.minValue will be mapped to ISize.minValue.

This function is overridden at runtime with an efficient implementation.

Equations

• a.abs = { toUSize := { toBitVec := a.toBitVec.abs } }

@[extern lean_isize_dec_eq]

def ISize.decEq (a b : ISize) : Decidable (a = b)

Decides whether two word-sized signed integers are equal. Usually accessed via the DecidableEq ISize instance.

This function is overridden at runtime with an efficient implementation.

Examples:

• ISize.decEq 123 123 = .isTrue rfl
• (if ((-7) : ISize) = 7 then "yes" else "no") = "no"
• show (7 : ISize) = 7 by decide

Equations

• { toUSize := n }.decEq { toUSize := m } = if h : n = m then isTrue ⋯ else isFalse ⋯

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

Strict inequality of word-sized signed integers, defined as inequality of the corresponding integers. Usually accessed via the < operator.

Equations

• a.lt b = (a.toBitVec.slt b.toBitVec = true)

def ISize.le (a b : ISize) : Prop

Non-strict inequality of word-sized signed integers, defined as inequality of the corresponding integers. Usually accessed via the ≤ operator.

Equations

• a.le b = (a.toBitVec.sle b.toBitVec = true)

instance instInhabitedISize : Inhabited ISize

Equations

• instInhabitedISize = { default := 0 }

instance instAddISize : Add ISize

Equations

• instAddISize = { add := ISize.add }

instance instSubISize : Sub ISize

Equations

• instSubISize = { sub := ISize.sub }

instance instMulISize : Mul ISize

Equations

• instMulISize = { mul := ISize.mul }

instance instModISize : Mod ISize

Equations

• instModISize = { mod := ISize.mod }

instance instDivISize : Div ISize

Equations

• instDivISize = { div := ISize.div }

instance instLTISize : LT ISize

Equations

• instLTISize = { lt := ISize.lt }

instance instLEISize : LE ISize

Equations

• instLEISize = { le := ISize.le }

instance instComplementISize : Complement ISize

Equations

• instComplementISize = { complement := ISize.complement }

instance instAndOpISize : AndOp ISize

Equations

• instAndOpISize = { and := ISize.land }

instance instOrOpISize : OrOp ISize

Equations

• instOrOpISize = { or := ISize.lor }

instance instXorISize : Xor ISize

Equations

• instXorISize = { xor := ISize.xor }

instance instShiftLeftISize : ShiftLeft ISize

Equations

• instShiftLeftISize = { shiftLeft := ISize.shiftLeft }

instance instShiftRightISize : ShiftRight ISize

Equations

• instShiftRightISize = { shiftRight := ISize.shiftRight }

instance instDecidableEqISize : DecidableEq ISize

Equations

• instDecidableEqISize = ISize.decEq

@[extern lean_bool_to_isize]

def Bool.toISize (b : Bool) : ISize

Converts true to 1 and false to 0.

Equations

• b.toISize = if b = true then 1 else 0

@[extern lean_isize_dec_lt]

def ISize.decLt (a b : ISize) : Decidable (a < b)

Decides whether one word-sized signed integer is strictly less than another. Usually accessed via the DecidableLT ISize instance.

This function is overridden at runtime with an efficient implementation.

Examples:

• (if ((-7) : ISize) < 7 then "yes" else "no") = "yes"
• (if (5 : ISize) < 5 then "yes" else "no") = "no"
• show ¬((7 : ISize) < 7) by decide

Equations

• a.decLt b = inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec = true))

@[extern lean_isize_dec_le]

def ISize.decLe (a b : ISize) : Decidable (a ≤ b)

Decides whether one word-sized signed integer is less than or equal to another. Usually accessed via the DecidableLE ISize instance.

This function is overridden at runtime with an efficient implementation.

Examples:

• (if ((-7) : ISize) ≤ 7 then "yes" else "no") = "yes"
• (if (15 : ISize) ≤ 15 then "yes" else "no") = "yes"
• (if (15 : ISize) ≤ 5 then "yes" else "no") = "no"
• show (7 : ISize) ≤ 7 by decide

Equations

• a.decLe b = inferInstanceAs (Decidable (a.toBitVec.sle b.toBitVec = true))

instance instDecidableLtISize (a b : ISize) : Decidable (a < b)

Equations

• instDecidableLtISize a b = a.decLt b

instance instDecidableLeISize (a b : ISize) : Decidable (a ≤ b)

Equations

• instDecidableLeISize a b = a.decLe b

instance instMaxISize : Max ISize

Equations

• instMaxISize = maxOfLe

instance instMinISize : Min ISize

Equations

• instMinISize = minOfLe