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.

• 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.

• 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.

• 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.

• 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.

• 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

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

@[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 instOfNatInt8 {n : Nat} : OfNat Int8 n

Equations

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

instance instNegInt8 : Neg Int8

Equations

• instNegInt8 = { neg := Int8.neg }

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

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

@[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 instOfNatInt16 {n : Nat} : OfNat Int16 n

Equations

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

instance instNegInt16 : Neg Int16

Equations

• instNegInt16 = { neg := Int16.neg }

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

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

@[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 instOfNatInt32 {n : Nat} : OfNat Int32 n

Equations

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

instance instNegInt32 : Neg Int32

Equations

• instNegInt32 = { neg := Int32.neg }

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

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

@[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 instOfNatInt64 {n : Nat} : OfNat Int64 n

Equations

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

instance instNegInt64 : Neg Int64

Equations

• instNegInt64 = { neg := Int64.neg }

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

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

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

Upcast ISize to Int64. This function is losless as ISize is either Int32 or Int64.

Equations

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

@[extern lean_int32_to_isize]

def Int32.toISize (a : Int32) : ISize

Upcast Int32 to ISize. This function is losless 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 instOfNatISize {n : Nat} : OfNat ISize n

Equations

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

instance instNegISize : Neg ISize

Equations

• instNegISize = { neg := ISize.neg }

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