def commandDeclare_int_theorems__ : Lean.ParserDescr

Equations

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

@[simp]

theorem Int8.toBitVec_ofNat {n : Nat} : (ofNat n).toBitVec = BitVec.ofNat 8 n

theorem Int8.ne_iff_toBitVec_ne {a b : Int8} : a ≠ b ↔ a.toBitVec ≠ b.toBitVec

theorem Int8.le_def {a b : Int8} : a ≤ b ↔ a.toBitVec.sle b.toBitVec = true

theorem Int8.eq_iff_toBitVec_eq {a b : Int8} : a = b ↔ a.toBitVec = b.toBitVec

theorem Int8.lt_def {a b : Int8} : a < b ↔ a.toBitVec.slt b.toBitVec = true

theorem Int8.toBitVec_inj {a b : Int8} : a.toBitVec = b.toBitVec ↔ a = b

@[simp]

theorem Int8.toBitVec_ofNatOfNat {n : Nat} : (OfNat.ofNat n).toBitVec = OfNat.ofNat n

theorem Int16.ne_iff_toBitVec_ne {a b : Int16} : a ≠ b ↔ a.toBitVec ≠ b.toBitVec

@[simp]

theorem Int16.toBitVec_ofNatOfNat {n : Nat} : (OfNat.ofNat n).toBitVec = OfNat.ofNat n

theorem Int16.le_def {a b : Int16} : a ≤ b ↔ a.toBitVec.sle b.toBitVec = true

theorem Int16.eq_iff_toBitVec_eq {a b : Int16} : a = b ↔ a.toBitVec = b.toBitVec

@[simp]

theorem Int16.toBitVec_ofNat {n : Nat} : (ofNat n).toBitVec = BitVec.ofNat 16 n

theorem Int16.toBitVec_inj {a b : Int16} : a.toBitVec = b.toBitVec ↔ a = b

theorem Int16.lt_def {a b : Int16} : a < b ↔ a.toBitVec.slt b.toBitVec = true

theorem Int32.toBitVec_inj {a b : Int32} : a.toBitVec = b.toBitVec ↔ a = b

theorem Int32.le_def {a b : Int32} : a ≤ b ↔ a.toBitVec.sle b.toBitVec = true

theorem Int32.lt_def {a b : Int32} : a < b ↔ a.toBitVec.slt b.toBitVec = true

theorem Int32.ne_iff_toBitVec_ne {a b : Int32} : a ≠ b ↔ a.toBitVec ≠ b.toBitVec

@[simp]

theorem Int32.toBitVec_ofNat {n : Nat} : (ofNat n).toBitVec = BitVec.ofNat 32 n

theorem Int32.eq_iff_toBitVec_eq {a b : Int32} : a = b ↔ a.toBitVec = b.toBitVec

@[simp]

theorem Int32.toBitVec_ofNatOfNat {n : Nat} : (OfNat.ofNat n).toBitVec = OfNat.ofNat n

theorem Int64.eq_iff_toBitVec_eq {a b : Int64} : a = b ↔ a.toBitVec = b.toBitVec

theorem Int64.lt_def {a b : Int64} : a < b ↔ a.toBitVec.slt b.toBitVec = true

@[simp]

theorem Int64.toBitVec_ofNat {n : Nat} : (ofNat n).toBitVec = BitVec.ofNat 64 n

@[simp]

theorem Int64.toBitVec_ofNatOfNat {n : Nat} : (OfNat.ofNat n).toBitVec = OfNat.ofNat n

theorem Int64.le_def {a b : Int64} : a ≤ b ↔ a.toBitVec.sle b.toBitVec = true

theorem Int64.ne_iff_toBitVec_ne {a b : Int64} : a ≠ b ↔ a.toBitVec ≠ b.toBitVec

theorem Int64.toBitVec_inj {a b : Int64} : a.toBitVec = b.toBitVec ↔ a = b

theorem ISize.eq_iff_toBitVec_eq {a b : ISize} : a = b ↔ a.toBitVec = b.toBitVec

theorem ISize.le_def {a b : ISize} : a ≤ b ↔ a.toBitVec.sle b.toBitVec = true

@[simp]

theorem ISize.toBitVec_ofNatOfNat {n : Nat} : (OfNat.ofNat n).toBitVec = OfNat.ofNat n

theorem ISize.ne_iff_toBitVec_ne {a b : ISize} : a ≠ b ↔ a.toBitVec ≠ b.toBitVec

theorem ISize.toBitVec_inj {a b : ISize} : a.toBitVec = b.toBitVec ↔ a = b

@[simp]

theorem ISize.toBitVec_ofNat {n : Nat} : (ofNat n).toBitVec = BitVec.ofNat System.Platform.numBits n

theorem ISize.lt_def {a b : ISize} : a < b ↔ a.toBitVec.slt b.toBitVec = true

@[simp]

theorem UInt8.toBitVec_toInt8 (x : UInt8) : x.toInt8.toBitVec = x.toBitVec

@[simp]

theorem UInt16.toBitVec_toInt16 (x : UInt16) : x.toInt16.toBitVec = x.toBitVec

@[simp]

theorem UInt32.toBitVec_toInt32 (x : UInt32) : x.toInt32.toBitVec = x.toBitVec

@[simp]

theorem UInt64.toBitVec_toInt64 (x : UInt64) : x.toInt64.toBitVec = x.toBitVec

@[simp]

theorem USize.toBitVec_toISize (x : USize) : x.toISize.toBitVec = x.toBitVec

@[simp]

theorem Int8.ofBitVec_uInt8ToBitVec (x : UInt8) : ofBitVec x.toBitVec = x.toInt8

@[simp]

theorem Int16.ofBitVec_uInt16ToBitVec (x : UInt16) : ofBitVec x.toBitVec = x.toInt16

@[simp]

theorem Int32.ofBitVec_uInt32ToBitVec (x : UInt32) : ofBitVec x.toBitVec = x.toInt32

@[simp]

theorem Int64.ofBitVec_uInt64ToBitVec (x : UInt64) : ofBitVec x.toBitVec = x.toInt64

@[simp]

theorem ISize.ofBitVec_uSize8ToBitVec (x : USize) : ofBitVec x.toBitVec = x.toISize

@[simp]

theorem UInt8.toUInt8_toInt8 (x : UInt8) : x.toInt8.toUInt8 = x

@[simp]

theorem UInt16.toUInt16_toInt16 (x : UInt16) : x.toInt16.toUInt16 = x

@[simp]

theorem UInt32.toUInt32_toInt32 (x : UInt32) : x.toInt32.toUInt32 = x

@[simp]

theorem UInt64.toUInt64_toInt64 (x : UInt64) : x.toInt64.toUInt64 = x

@[simp]

theorem USize.toUSize_toISize (x : USize) : x.toISize.toUSize = x

@[simp]

theorem ISize.toBitVec_neg (x : ISize) : (-x).toBitVec = -x.toBitVec

@[simp]

theorem ISize.toBitVec_zero : toBitVec 0 = 0

@[simp]

theorem ISize.toBitVec_ofInt (i : Int) : (ofInt i).toBitVec = BitVec.ofInt System.Platform.numBits i

@[simp]

theorem Int8.neg_zero : -0 = 0

@[simp]

theorem Int16.neg_zero : -0 = 0

@[simp]

theorem Int32.neg_zero : -0 = 0

@[simp]

theorem Int64.neg_zero : -0 = 0

@[simp]

theorem ISize.neg_zero : -0 = 0

theorem ISize.toNat_toBitVec_ofNat_of_lt {n : Nat} (h : n < 2 ^ 32) : (ofNat n).toBitVec.toNat = n

theorem ISize.toInt_ofInt {n : Int} (hn : -2 ^ 31 ≤ n) (hn' : n < 2 ^ 31) : (ofInt n).toInt = n

theorem ISize.toNatClampNeg_ofInt_eq_zero {n : Int} (hn : -2 ^ 31 ≤ n) (hn' : n ≤ 0) : (ofInt n).toNatClampNeg = 0

theorem ISize.neg_ofInt {n : Int} : -ofInt n = ofInt (-n)

theorem ISize.ofInt_eq_ofNat {n : Nat} : ofInt ↑n = ofNat n

theorem ISize.neg_ofNat {n : Nat} : -ofNat n = ofInt (-↑n)

theorem ISize.toNatClampNeg_ofNat_of_lt {n : Nat} (h : n < 2 ^ 31) : (ofNat n).toNatClampNeg = n

theorem ISize.toNatClampNeg_neg_ofNat_of_le {n : Nat} (h : n ≤ 2 ^ 31) : (-ofNat n).toNatClampNeg = 0

theorem ISize.toInt_ofNat_of_lt {n : Nat} (h : n < 2 ^ 31) : (ofNat n).toInt = ↑n

theorem ISize.toInt_neg_ofNat_of_le {n : Nat} (h : n ≤ 2 ^ 31) : (-ofNat n).toInt = -↑n