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.

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

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

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 : Int8) (b : Int8) : Int8

Equations

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

@[extern lean_int8_sub]

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

Equations

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

@[extern lean_int8_mul]

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

Equations

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

@[extern lean_int8_div]

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

Equations

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

@[extern lean_int8_mod]

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

Equations

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

@[extern lean_int8_land]

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

Equations

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

@[extern lean_int8_lor]

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

Equations

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

@[extern lean_int8_xor]

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

Equations

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

@[extern lean_int8_shift_left]

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

Equations

• a.shiftLeft b = { toUInt8 := { toBitVec := a.toBitVec <<< (b.mod 8).toBitVec } }

@[extern lean_int8_shift_right]

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

Equations

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

@[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 : Int8) (b : Int8) : Decidable (a = b)

Equations

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

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

Equations

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

def Int8.le (a : Int8) (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_int8_dec_lt]

def Int8.decLt (a : Int8) (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 : Int8) (b : Int8) : Decidable (a ≤ b)

Equations

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

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

Equations

• instDecidableLtInt8 a b = a.decLt b

instance instDecidableLeInt8 (a : Int8) (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