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

The type of signed 8-bit integers. This type has special support in the compiler to make it actually 8 bits rather than wrapping a Nat.

• ofUInt8 :: (
• toUInt8 : UInt8

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

• )

structure Int16 : Type

The type of signed 16-bit integers. This type has special support in the compiler to make it actually 16 bits rather than wrapping a Nat.

• ofUInt16 :: (
• toUInt16 : UInt16

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

• )

structure Int32 : Type

The type of signed 32-bit integers. This type has special support in the compiler to make it actually 32 bits rather than wrapping a Nat.

• ofUInt32 :: (
• toUInt32 : UInt32

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

• )

structure Int64 : Type

The type of signed 64-bit integers. This type has special support in the compiler to make it actually 64 bits rather than wrapping a Nat.

• ofUInt64 :: (
• toUInt64 : UInt64

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

• )

structure ISize : Type

A ISize is a signed integer with the size of a word for the platform's architecture.

For example, if running on a 32-bit machine, ISize is equivalent to Int32. Or on a 64-bit machine, Int64.

• ofUSize :: (
• toUSize : USize

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

• )

@[reducible, inline]

abbrev Int8.size : Nat

The size of type 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

Equations

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

@[extern lean_int8_of_nat]

def Int8.ofNat (n : Nat) : Int8

Equations

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

@[reducible, inline]

abbrev Int.toInt8 (i : Int) : Int8

Equations

• Int.toInt8 = Int8.ofInt

@[reducible, inline]

abbrev Nat.toInt8 (n : Nat) : Int8

Equations

• Nat.toInt8 = Int8.ofNat

@[extern lean_int8_to_int]

def Int8.toInt (i : Int8) : Int

Equations

• i.toInt = i.toBitVec.toInt

@[inline]

def Int8.toNatClampNeg (i : Int8) : Nat

This function has the same behavior as Int.toNat for negative numbers. If you want to obtain the 2's complement representation use toBitVec.

Equations

• i.toNatClampNeg = i.toInt.toNat

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

def Int8.toNat (i : Int8) : Nat

This function has the same behavior as Int.toNat for negative numbers. If you want to obtain the 2's complement representation use toBitVec.

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

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 maximum value an Int8 may attain, that is, 2^7 - 1 = 127.

Equations

• Int8.maxValue = 127

@[reducible, inline]

abbrev Int8.minValue : Int8

The minimum value an Int8 may attain, that is, -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 which 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

Equations

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

@[extern lean_int8_sub]

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

Equations

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

@[extern lean_int8_mul]

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

Equations

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

@[extern lean_int8_div]

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

Equations

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

@[extern lean_int8_mod]

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

Equations

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

@[extern lean_int8_land]

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

Equations

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

@[extern lean_int8_lor]

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

Equations

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

@[extern lean_int8_xor]

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

Equations

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

@[extern lean_int8_shift_left]

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

Equations

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

@[extern lean_int8_shift_right]

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

Equations

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

@[extern lean_int8_complement]

def Int8.complement (a : Int8) : Int8

Equations

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

@[extern lean_int8_abs]

def Int8.abs (a : Int8) : Int8

Computes the absolute value of the 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.

Equations

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

@[extern lean_int8_dec_eq]

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

Equations

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

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

Equations

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

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

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

Equations

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

@[extern lean_int8_dec_lt]

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

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)

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 size of type 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

Equations

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

@[extern lean_int16_of_nat]

def Int16.ofNat (n : Nat) : Int16

Equations

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

@[reducible, inline]

abbrev Int.toInt16 (i : Int) : Int16

Equations

• Int.toInt16 = Int16.ofInt

@[reducible, inline]

abbrev Nat.toInt16 (n : Nat) : Int16

Equations

• Nat.toInt16 = Int16.ofNat

@[extern lean_int16_to_int]

def Int16.toInt (i : Int16) : Int

Equations

• i.toInt = i.toBitVec.toInt

@[inline]

def Int16.toNatClampNeg (i : Int16) : Nat

This function has the same behavior as Int.toNat for negative numbers. If you want to obtain the 2's complement representation use toBitVec.

Equations

• i.toNatClampNeg = i.toInt.toNat

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

def Int16.toNat (i : Int16) : Nat

This function has the same behavior as Int.toNat for negative numbers. If you want to obtain the 2's complement representation use toBitVec.

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

Equations

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

@[extern lean_int8_to_int16]

def Int8.toInt16 (a : Int8) : Int16

Equations

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

@[extern lean_int16_neg]

def Int16.neg (i : Int16) : Int16

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 maximum value an Int16 may attain, that is, 2^15 - 1 = 32767.

Equations

• Int16.maxValue = 32767

@[reducible, inline]

abbrev Int16.minValue : Int16

The minimum value an Int16 may attain, that is, -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 which 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

Equations

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

@[extern lean_int16_sub]

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

Equations

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

@[extern lean_int16_mul]

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

Equations

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

@[extern lean_int16_div]

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

Equations

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

@[extern lean_int16_mod]

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

Equations

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

@[extern lean_int16_land]

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

Equations

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

@[extern lean_int16_lor]

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

Equations

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

@[extern lean_int16_xor]

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

Equations

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

@[extern lean_int16_shift_left]

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

Equations

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

@[extern lean_int16_shift_right]

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

Equations

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

@[extern lean_int16_complement]

def Int16.complement (a : Int16) : Int16

Equations

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

@[extern lean_int16_abs]

def Int16.abs (a : Int16) : Int16

Computes the absolute value of the 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.

Equations

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

@[extern lean_int16_dec_eq]

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

Equations

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

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

Equations

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

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

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

Equations

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

@[extern lean_int16_dec_lt]

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

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)

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 size of type 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

Equations

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

@[extern lean_int32_of_nat]

def Int32.ofNat (n : Nat) : Int32

Equations

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

@[reducible, inline]

abbrev Int.toInt32 (i : Int) : Int32

Equations

• Int.toInt32 = Int32.ofInt

@[reducible, inline]

abbrev Nat.toInt32 (n : Nat) : Int32

Equations

• Nat.toInt32 = Int32.ofNat

@[extern lean_int32_to_int]

def Int32.toInt (i : Int32) : Int

Equations

• i.toInt = i.toBitVec.toInt

@[inline]

def Int32.toNatClampNeg (i : Int32) : Nat

This function has the same behavior as Int.toNat for negative numbers. If you want to obtain the 2's complement representation use toBitVec.

Equations

• i.toNatClampNeg = i.toInt.toNat

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

def Int32.toNat (i : Int32) : Nat

This function has the same behavior as Int.toNat for negative numbers. If you want to obtain the 2's complement representation use toBitVec.

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

Equations

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

@[extern lean_int32_to_int16]

def Int32.toInt16 (a : Int32) : Int16

Equations

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

@[extern lean_int8_to_int32]

def Int8.toInt32 (a : Int8) : Int32

Equations

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

@[extern lean_int16_to_int32]

def Int16.toInt32 (a : Int16) : Int32

Equations

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

@[extern lean_int32_neg]

def Int32.neg (i : Int32) : Int32

Equations

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

instance instToStringInt32 : ToString Int32

Equations

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

instance instReprInt16_1 : Repr Int16

Equations

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

instance instReprAtomInt16_1 : ReprAtom Int16

Equations

• instReprAtomInt16_1 = { }

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 maximum value an Int32 may attain, that is, 2^31 - 1 = 2147483647.

Equations

• Int32.maxValue = 2147483647

@[reducible, inline]

abbrev Int32.minValue : Int32

The minimum value an Int32 may attain, that is, -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 which 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

Equations

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

@[extern lean_int32_sub]

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

Equations

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

@[extern lean_int32_mul]

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

Equations

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

@[extern lean_int32_div]

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

Equations

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

@[extern lean_int32_mod]

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

Equations

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

@[extern lean_int32_land]

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

Equations

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

@[extern lean_int32_lor]

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

Equations

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

@[extern lean_int32_xor]

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

Equations

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

@[extern lean_int32_shift_left]

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

Equations

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

@[extern lean_int32_shift_right]

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

Equations

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

@[extern lean_int32_complement]

def Int32.complement (a : Int32) : Int32

Equations

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

@[extern lean_int32_abs]

def Int32.abs (a : Int32) : Int32

Computes the absolute value of the 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.

Equations

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

@[extern lean_int32_dec_eq]

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

Equations

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

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

Equations

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

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

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

Equations

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

@[extern lean_int32_dec_lt]

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

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)

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 size of type 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

Equations

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

@[extern lean_int64_of_nat]

def Int64.ofNat (n : Nat) : Int64

Equations

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

@[reducible, inline]

abbrev Int.toInt64 (i : Int) : Int64

Equations

• Int.toInt64 = Int64.ofInt

@[reducible, inline]

abbrev Nat.toInt64 (n : Nat) : Int64

Equations

• Nat.toInt64 = Int64.ofNat

@[extern lean_int64_to_int_sint]

def Int64.toInt (i : Int64) : Int

Equations

• i.toInt = i.toBitVec.toInt

@[inline]

def Int64.toNatClampNeg (i : Int64) : Nat

This function has the same behavior as Int.toNat for negative numbers. If you want to obtain the 2's complement representation use toBitVec.

Equations

• i.toNatClampNeg = i.toInt.toNat

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

def Int64.toNat (i : Int64) : Nat

This function has the same behavior as Int.toNat for negative numbers. If you want to obtain the 2's complement representation use toBitVec.

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

Equations

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

@[extern lean_int64_to_int16]

def Int64.toInt16 (a : Int64) : Int16

Equations

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

@[extern lean_int64_to_int32]

def Int64.toInt32 (a : Int64) : Int32

Equations

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

@[extern lean_int8_to_int64]

def Int8.toInt64 (a : Int8) : Int64

Equations

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

@[extern lean_int16_to_int64]

def Int16.toInt64 (a : Int16) : Int64

Equations

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

@[extern lean_int32_to_int64]

def Int32.toInt64 (a : Int32) : Int64

Equations

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

@[extern lean_int64_neg]

def Int64.neg (i : Int64) : Int64

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 maximum value an Int64 may attain, that is, 2^63 - 1 = 9223372036854775807.

Equations

• Int64.maxValue = 9223372036854775807

@[reducible, inline]

abbrev Int64.minValue : Int64

The minimum value an Int64 may attain, that is, -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 which 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

Equations

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

@[extern lean_int64_sub]

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

Equations

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

@[extern lean_int64_mul]

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

Equations

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

@[extern lean_int64_div]

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

Equations

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

@[extern lean_int64_mod]

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

Equations

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

@[extern lean_int64_land]

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

Equations

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

@[extern lean_int64_lor]

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

Equations

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

@[extern lean_int64_xor]

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

Equations

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

@[extern lean_int64_shift_left]

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

Equations

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

@[extern lean_int64_shift_right]

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

Equations

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

@[extern lean_int64_complement]

def Int64.complement (a : Int64) : Int64

Equations

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

@[extern lean_int64_abs]

def Int64.abs (a : Int64) : Int64

Computes the absolute value of the 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.

Equations

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

@[extern lean_int64_dec_eq]

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

Equations

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

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

Equations

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

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

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

Equations

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

@[extern lean_int64_dec_lt]

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

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)

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 size of type 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

Equations

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

@[extern lean_isize_of_nat]

def ISize.ofNat (n : Nat) : ISize

Equations

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

@[reducible, inline]

abbrev Int.toISize (i : Int) : ISize

Equations

• Int.toISize = ISize.ofInt

@[reducible, inline]

abbrev Nat.toISize (n : Nat) : ISize

Equations

• Nat.toISize = ISize.ofNat

@[extern lean_isize_to_int]

def ISize.toInt (i : ISize) : Int

Equations

• i.toInt = i.toBitVec.toInt

@[inline]

def ISize.toNatClampNeg (i : ISize) : Nat

This function has the same behavior as Int.toNat for negative numbers. If you want to obtain the 2's complement representation use toBitVec.

Equations

• i.toNatClampNeg = i.toInt.toNat

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

def ISize.toNat (i : ISize) : Nat

This function has the same behavior as Int.toNat for negative numbers. If you want to obtain the 2's complement representation use toBitVec.

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

Equations

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

@[extern lean_isize_to_int16]

def ISize.toInt16 (a : ISize) : Int16

Equations

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

@[extern lean_isize_to_int32]

def ISize.toInt32 (a : ISize) : Int32

Equations

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

@[extern lean_isize_to_int64]

def ISize.toInt64 (a : ISize) : Int64

Upcasts ISize to Int64. This function is lossless as ISize is either Int32 or Int64.

Equations

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

@[extern lean_int8_to_isize]

def Int8.toISize (a : Int8) : ISize

Equations

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

@[extern lean_int16_to_isize]

def Int16.toISize (a : Int16) : ISize

Equations

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

@[extern lean_int32_to_isize]

def Int32.toISize (a : Int32) : ISize

Upcasts Int32 to ISize. This function is lossless as ISize is either Int32 or Int64.

Equations

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

@[extern lean_int64_to_isize]

def Int64.toISize (a : Int64) : ISize

Equations

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

@[extern lean_isize_neg]

def ISize.neg (i : ISize) : ISize

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 maximum value an ISize may attain, that is, 2^(System.Platform.numBits - 1) - 1.

Equations

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

@[reducible, inline]

abbrev ISize.minValue : ISize

The minimum value an ISize may attain, that is, -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 which 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

Equations

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

@[extern lean_isize_sub]

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

Equations

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

@[extern lean_isize_mul]

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

Equations

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

@[extern lean_isize_div]

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

Equations

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

@[extern lean_isize_mod]

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

Equations

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

@[extern lean_isize_land]

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

Equations

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

@[extern lean_isize_lor]

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

Equations

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

@[extern lean_isize_xor]

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

Equations

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

@[extern lean_isize_shift_left]

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

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

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

Equations

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

@[extern lean_isize_abs]

def ISize.abs (a : ISize) : ISize

Computes the absolute value of the 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.

Equations

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

@[extern lean_isize_dec_eq]

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

Equations

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

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

Equations

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

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

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

Equations

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

@[extern lean_isize_dec_lt]

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

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)

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