source
def commandDeclare_int_theorems__ :
Lean.ParserDescr
Equations

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

Instances For

source
theorem Int8.eq_iff_toBitVec_eq {a b : Int8} :
a = b ↔ a.toBitVec = b.toBitVec
source
theorem Int8.ofBitVec_inj {a b : BitVec 8} :
ofBitVec a = ofBitVec b ↔ a = b
source
@[simp]
theorem Int8.toBitVec_div {a b : Int8} :
(a / b).toBitVec = a.toBitVec.sdiv b.toBitVec
source
@[simp]
theorem Int8.toBitVec_sub {a b : Int8} :
(a - b).toBitVec = a.toBitVec - b.toBitVec
source
@[simp]
theorem Int8.toBitVec_mod {a b : Int8} :
(a % b).toBitVec = a.toBitVec.srem b.toBitVec
source
@[simp]
theorem Int8.toBitVec_ofNat' {n : Nat} :
(ofNat n).toBitVec = BitVec.ofNat 8 n
source
theorem Int8.eq_iff_ofBitVec_eq {a b : BitVec 8} :
a = b ↔ ofBitVec a = ofBitVec b
source
@[simp]
theorem Int8.toBitVec_mul {a b : Int8} :
(a * b).toBitVec = a.toBitVec * b.toBitVec
source
theorem Int8.ne_iff_toBitVec_ne {a b : Int8} :
a ≠ b ↔ a.toBitVec ≠ b.toBitVec
source
theorem Int8.lt_iff_toBitVec_slt {a b : Int8} :
a < b ↔ a.toBitVec.slt b.toBitVec = true
source
@[simp]
theorem Int8.toBitVec_ofNat {n : Nat} :
(OfNat.ofNat n).toBitVec = OfNat.ofNat n
source
theorem Int8.le_iff_toBitVec_sle {a b : Int8} :
a ≤ b ↔ a.toBitVec.sle b.toBitVec = true
source
theorem Int8.ne_iff_ofBitVec_ne {a b : BitVec 8} :
a ≠ b ↔ ofBitVec a ≠ ofBitVec b
source
theorem Int8.toBitVec_inj {a b : Int8} :
a.toBitVec = b.toBitVec ↔ a = b
source
@[simp]
theorem Int8.toBitVec_add {a b : Int8} :
(a + b).toBitVec = a.toBitVec + b.toBitVec
source
@[simp]
theorem Int16.toBitVec_div {a b : Int16} :
(a / b).toBitVec = a.toBitVec.sdiv b.toBitVec
source
@[simp]
theorem Int16.toBitVec_ofNat {n : Nat} :
(OfNat.ofNat n).toBitVec = OfNat.ofNat n
source
theorem Int16.lt_iff_toBitVec_slt {a b : Int16} :
a < b ↔ a.toBitVec.slt b.toBitVec = true
source
@[simp]
theorem Int16.toBitVec_mod {a b : Int16} :
(a % b).toBitVec = a.toBitVec.srem b.toBitVec
source
@[simp]
theorem Int16.toBitVec_mul {a b : Int16} :
(a * b).toBitVec = a.toBitVec * b.toBitVec
source
theorem Int16.ofBitVec_inj {a b : BitVec 16} :
ofBitVec a = ofBitVec b ↔ a = b
source
theorem Int16.ne_iff_ofBitVec_ne {a b : BitVec 16} :
a ≠ b ↔ ofBitVec a ≠ ofBitVec b
source
theorem Int16.le_iff_toBitVec_sle {a b : Int16} :
a ≤ b ↔ a.toBitVec.sle b.toBitVec = true
source
@[simp]
theorem Int16.toBitVec_add {a b : Int16} :
(a + b).toBitVec = a.toBitVec + b.toBitVec
source
theorem Int16.eq_iff_ofBitVec_eq {a b : BitVec 16} :
a = b ↔ ofBitVec a = ofBitVec b
source
theorem Int16.ne_iff_toBitVec_ne {a b : Int16} :
a ≠ b ↔ a.toBitVec ≠ b.toBitVec
source
theorem Int16.eq_iff_toBitVec_eq {a b : Int16} :
a = b ↔ a.toBitVec = b.toBitVec
source
@[simp]
theorem Int16.toBitVec_sub {a b : Int16} :
(a - b).toBitVec = a.toBitVec - b.toBitVec
source
@[simp]
theorem Int16.toBitVec_ofNat' {n : Nat} :
(ofNat n).toBitVec = BitVec.ofNat 16 n
source
theorem Int16.toBitVec_inj {a b : Int16} :
a.toBitVec = b.toBitVec ↔ a = b
source
@[simp]
theorem Int32.toBitVec_sub {a b : Int32} :
(a - b).toBitVec = a.toBitVec - b.toBitVec
source
@[simp]
theorem Int32.toBitVec_mod {a b : Int32} :
(a % b).toBitVec = a.toBitVec.srem b.toBitVec
source
@[simp]
theorem Int32.toBitVec_div {a b : Int32} :
(a / b).toBitVec = a.toBitVec.sdiv b.toBitVec
source
theorem Int32.ofBitVec_inj {a b : BitVec 32} :
ofBitVec a = ofBitVec b ↔ a = b
source
theorem Int32.lt_iff_toBitVec_slt {a b : Int32} :
a < b ↔ a.toBitVec.slt b.toBitVec = true
source
@[simp]
theorem Int32.toBitVec_ofNat {n : Nat} :
(OfNat.ofNat n).toBitVec = OfNat.ofNat n
source
@[simp]
theorem Int32.toBitVec_add {a b : Int32} :
(a + b).toBitVec = a.toBitVec + b.toBitVec
source
theorem Int32.eq_iff_ofBitVec_eq {a b : BitVec 32} :
a = b ↔ ofBitVec a = ofBitVec b
source
theorem Int32.le_iff_toBitVec_sle {a b : Int32} :
a ≤ b ↔ a.toBitVec.sle b.toBitVec = true
source
theorem Int32.eq_iff_toBitVec_eq {a b : Int32} :
a = b ↔ a.toBitVec = b.toBitVec
source
@[simp]
theorem Int32.toBitVec_ofNat' {n : Nat} :
(ofNat n).toBitVec = BitVec.ofNat 32 n
source
theorem Int32.ne_iff_toBitVec_ne {a b : Int32} :
a ≠ b ↔ a.toBitVec ≠ b.toBitVec
source
theorem Int32.toBitVec_inj {a b : Int32} :
a.toBitVec = b.toBitVec ↔ a = b
source
@[simp]
theorem Int32.toBitVec_mul {a b : Int32} :
(a * b).toBitVec = a.toBitVec * b.toBitVec
source
theorem Int32.ne_iff_ofBitVec_ne {a b : BitVec 32} :
a ≠ b ↔ ofBitVec a ≠ ofBitVec b
source
theorem Int64.eq_iff_toBitVec_eq {a b : Int64} :
a = b ↔ a.toBitVec = b.toBitVec
source
theorem Int64.ne_iff_toBitVec_ne {a b : Int64} :
a ≠ b ↔ a.toBitVec ≠ b.toBitVec
source
theorem Int64.ne_iff_ofBitVec_ne {a b : BitVec 64} :
a ≠ b ↔ ofBitVec a ≠ ofBitVec b
source
theorem Int64.ofBitVec_inj {a b : BitVec 64} :
ofBitVec a = ofBitVec b ↔ a = b
source
@[simp]
theorem Int64.toBitVec_mul {a b : Int64} :
(a * b).toBitVec = a.toBitVec * b.toBitVec
source
theorem Int64.le_iff_toBitVec_sle {a b : Int64} :
a ≤ b ↔ a.toBitVec.sle b.toBitVec = true
source
@[simp]
theorem Int64.toBitVec_sub {a b : Int64} :
(a - b).toBitVec = a.toBitVec - b.toBitVec
source
@[simp]
theorem Int64.toBitVec_div {a b : Int64} :
(a / b).toBitVec = a.toBitVec.sdiv b.toBitVec
source
theorem Int64.eq_iff_ofBitVec_eq {a b : BitVec 64} :
a = b ↔ ofBitVec a = ofBitVec b
source
theorem Int64.lt_iff_toBitVec_slt {a b : Int64} :
a < b ↔ a.toBitVec.slt b.toBitVec = true
source
@[simp]
theorem Int64.toBitVec_ofNat' {n : Nat} :
(ofNat n).toBitVec = BitVec.ofNat 64 n
source
theorem Int64.toBitVec_inj {a b : Int64} :
a.toBitVec = b.toBitVec ↔ a = b
source
@[simp]
theorem Int64.toBitVec_ofNat {n : Nat} :
(OfNat.ofNat n).toBitVec = OfNat.ofNat n
source
@[simp]
theorem Int64.toBitVec_add {a b : Int64} :
(a + b).toBitVec = a.toBitVec + b.toBitVec
source
@[simp]
theorem Int64.toBitVec_mod {a b : Int64} :
(a % b).toBitVec = a.toBitVec.srem b.toBitVec
source
theorem ISize.ne_iff_ofBitVec_ne {a b : BitVec System.Platform.numBits} :
a ≠ b ↔ ofBitVec a ≠ ofBitVec b
source
@[simp]
theorem ISize.toBitVec_ofNat {n : Nat} :
(OfNat.ofNat n).toBitVec = OfNat.ofNat n
source
theorem ISize.le_iff_toBitVec_sle {a b : ISize} :
a ≤ b ↔ a.toBitVec.sle b.toBitVec = true
source
@[simp]
theorem ISize.toBitVec_div {a b : ISize} :
(a / b).toBitVec = a.toBitVec.sdiv b.toBitVec
source
theorem ISize.ne_iff_toBitVec_ne {a b : ISize} :
a ≠ b ↔ a.toBitVec ≠ b.toBitVec
source
@[simp]
theorem ISize.toBitVec_add {a b : ISize} :
(a + b).toBitVec = a.toBitVec + b.toBitVec
source
@[simp]
theorem ISize.toBitVec_ofNat' {n : Nat} :
(ofNat n).toBitVec = BitVec.ofNat System.Platform.numBits n
source
theorem ISize.toBitVec_inj {a b : ISize} :
a.toBitVec = b.toBitVec ↔ a = b
source
@[simp]
theorem ISize.toBitVec_sub {a b : ISize} :
(a - b).toBitVec = a.toBitVec - b.toBitVec
source
theorem ISize.eq_iff_ofBitVec_eq {a b : BitVec System.Platform.numBits} :
a = b ↔ ofBitVec a = ofBitVec b
source
@[simp]
theorem ISize.toBitVec_mod {a b : ISize} :
(a % b).toBitVec = a.toBitVec.srem b.toBitVec
source
@[simp]
theorem ISize.toBitVec_mul {a b : ISize} :
(a * b).toBitVec = a.toBitVec * b.toBitVec
source
theorem ISize.ofBitVec_inj {a b : BitVec System.Platform.numBits} :
ofBitVec a = ofBitVec b ↔ a = b
source
theorem ISize.lt_iff_toBitVec_slt {a b : ISize} :
a < b ↔ a.toBitVec.slt b.toBitVec = true
source
theorem ISize.eq_iff_toBitVec_eq {a b : ISize} :
a = b ↔ a.toBitVec = b.toBitVec
source
@[deprecated Int8.le_iff_toBitVec_sle (since := "2025-03-20")]
theorem Int8.le_def {a b : Int8} :
a ≤ b ↔ a.toBitVec.sle b.toBitVec = true
source
@[deprecated Int16.le_iff_toBitVec_sle (since := "2025-03-20")]
theorem Int16.le_def {a b : Int16} :
a ≤ b ↔ a.toBitVec.sle b.toBitVec = true
source
@[deprecated Int32.le_iff_toBitVec_sle (since := "2025-03-20")]
theorem Int32.le_def {a b : Int32} :
a ≤ b ↔ a.toBitVec.sle b.toBitVec = true
source
@[deprecated Int64.le_iff_toBitVec_sle (since := "2025-03-20")]
theorem Int64.le_def {a b : Int64} :
a ≤ b ↔ a.toBitVec.sle b.toBitVec = true
source
@[deprecated ISize.le_iff_toBitVec_sle (since := "2025-03-20")]
theorem ISize.le_def {a b : ISize} :
a ≤ b ↔ a.toBitVec.sle b.toBitVec = true
source
@[deprecated Int8.lt_iff_toBitVec_slt (since := "2025-03-20")]
theorem Int8.lt_def {a b : Int8} :
a < b ↔ a.toBitVec.slt b.toBitVec = true
source
@[deprecated Int16.lt_iff_toBitVec_slt (since := "2025-03-20")]
theorem Int16.lt_def {a b : Int16} :
a < b ↔ a.toBitVec.slt b.toBitVec = true
source
@[deprecated Int32.lt_iff_toBitVec_slt (since := "2025-03-20")]
theorem Int32.lt_def {a b : Int32} :
a < b ↔ a.toBitVec.slt b.toBitVec = true
source
@[deprecated Int64.lt_iff_toBitVec_slt (since := "2025-03-20")]
theorem Int64.lt_def {a b : Int64} :
a < b ↔ a.toBitVec.slt b.toBitVec = true
source
@[deprecated ISize.lt_iff_toBitVec_slt (since := "2025-03-20")]
theorem ISize.lt_def {a b : ISize} :
a < b ↔ a.toBitVec.slt b.toBitVec = true
source
theorem Int8.toInt.inj {x y : Int8} (h : x.toInt = y.toInt) :
x = y
source
theorem Int8.toInt_inj {x y : Int8} :
x.toInt = y.toInt ↔ x = y
source
theorem Int16.toInt.inj {x y : Int16} (h : x.toInt = y.toInt) :
x = y
source
theorem Int16.toInt_inj {x y : Int16} :
x.toInt = y.toInt ↔ x = y
source
theorem Int32.toInt.inj {x y : Int32} (h : x.toInt = y.toInt) :
x = y
source
theorem Int32.toInt_inj {x y : Int32} :
x.toInt = y.toInt ↔ x = y
source
theorem Int64.toInt.inj {x y : Int64} (h : x.toInt = y.toInt) :
x = y
source
theorem Int64.toInt_inj {x y : Int64} :
x.toInt = y.toInt ↔ x = y
source
theorem ISize.toInt.inj {x y : ISize} (h : x.toInt = y.toInt) :
x = y
source
theorem ISize.toInt_inj {x y : ISize} :
x.toInt = y.toInt ↔ x = y
source
@[simp]
theorem Int8.toBitVec_neg (x : Int8) :
(-x).toBitVec = -x.toBitVec
source
@[simp]
theorem Int16.toBitVec_neg (x : Int16) :
(-x).toBitVec = -x.toBitVec
source
@[simp]
theorem Int32.toBitVec_neg (x : Int32) :
(-x).toBitVec = -x.toBitVec
source
@[simp]
theorem Int64.toBitVec_neg (x : Int64) :
(-x).toBitVec = -x.toBitVec
source
@[simp]
theorem ISize.toBitVec_neg (x : ISize) :
(-x).toBitVec = -x.toBitVec
source
@[simp]
theorem Int8.toBitVec_zero :
toBitVec 0 = 0#8
source
@[simp]
theorem Int16.toBitVec_zero :
toBitVec 0 = 0#16
source
@[simp]
theorem Int32.toBitVec_zero :
toBitVec 0 = 0#32
source
@[simp]
theorem Int64.toBitVec_zero :
toBitVec 0 = 0#64
source
@[simp]
theorem ISize.toBitVec_zero :
toBitVec 0 = 0#System.Platform.numBits
source
theorem Int8.toBitVec_one :
toBitVec 1 = 1#8
source
theorem Int16.toBitVec_one :
toBitVec 1 = 1#16
source
theorem Int32.toBitVec_one :
toBitVec 1 = 1#32
source
theorem Int64.toBitVec_one :
toBitVec 1 = 1#64
source
theorem ISize.toBitVec_one :
toBitVec 1 = 1#System.Platform.numBits
source
@[simp]
theorem Int8.toBitVec_ofInt (i : Int) :
(ofInt i).toBitVec = BitVec.ofInt 8 i
source
@[simp]
theorem Int16.toBitVec_ofInt (i : Int) :
(ofInt i).toBitVec = BitVec.ofInt 16 i
source
@[simp]
theorem Int32.toBitVec_ofInt (i : Int) :
(ofInt i).toBitVec = BitVec.ofInt 32 i
source
@[simp]
theorem Int64.toBitVec_ofInt (i : Int) :
(ofInt i).toBitVec = BitVec.ofInt 64 i
source
@[simp]
theorem ISize.toBitVec_ofInt (i : Int) :
(ofInt i).toBitVec = BitVec.ofInt System.Platform.numBits i
source
@[simp]
theorem Int8.neg_zero :
-0 = 0
source
@[simp]
theorem Int16.neg_zero :
-0 = 0
source
@[simp]
theorem Int32.neg_zero :
-0 = 0
source
@[simp]
theorem Int64.neg_zero :
-0 = 0
source
@[simp]
theorem ISize.neg_zero :
-0 = 0
source
theorem ISize.toNat_toBitVec_ofNat_of_lt {n : Nat} (h : n < 2 ^ 32) :
(ofNat n).toBitVec.toNat = n
source
@[simp]
theorem Int8.toInt_ofInt {n : Int} :
(ofInt n).toInt = n.bmod size
source
@[simp]
theorem Int16.toInt_ofInt {n : Int} :
(ofInt n).toInt = n.bmod size
source
@[simp]
theorem Int32.toInt_ofInt {n : Int} :
(ofInt n).toInt = n.bmod size
source
@[simp]
theorem Int64.toInt_ofInt {n : Int} :
(ofInt n).toInt = n.bmod size
source
theorem ISize.toInt_ofInt {n : Int} :
(ofInt n).toInt = n.bmod size
source
@[simp]
theorem Int8.toInt_ofNat' {n : Nat} :
(ofNat n).toInt = (↑n).bmod size
source
@[simp]
theorem Int16.toInt_ofNat' {n : Nat} :
(ofNat n).toInt = (↑n).bmod size
source
@[simp]
theorem Int32.toInt_ofNat' {n : Nat} :
(ofNat n).toInt = (↑n).bmod size
source
@[simp]
theorem Int64.toInt_ofNat' {n : Nat} :
(ofNat n).toInt = (↑n).bmod size
source
@[simp]
theorem ISize.toInt_ofNat' {n : Nat} :
(ofNat n).toInt = (↑n).bmod size
source
theorem Int8.toInt_ofNat {n : Nat} :
(OfNat.ofNat n).toInt = (↑n).bmod size
source
theorem Int16.toInt_ofNat {n : Nat} :
(OfNat.ofNat n).toInt = (↑n).bmod size
source
theorem Int32.toInt_ofNat {n : Nat} :
(OfNat.ofNat n).toInt = (↑n).bmod size
source
theorem Int64.toInt_ofNat {n : Nat} :
(OfNat.ofNat n).toInt = (↑n).bmod size
source
theorem ISize.toInt_ofNat {n : Nat} :
(OfNat.ofNat n).toInt = (↑n).bmod size
source
theorem Int8.toInt_ofInt_of_le {n : Int} (hn : -2 ^ 7 ≤ n) (hn' : n < 2 ^ 7) :
(ofInt n).toInt = n
source
theorem Int16.toInt_ofInt_of_le {n : Int} (hn : -2 ^ 15 ≤ n) (hn' : n < 2 ^ 15) :
(ofInt n).toInt = n
source
theorem Int32.toInt_ofInt_of_le {n : Int} (hn : -2 ^ 31 ≤ n) (hn' : n < 2 ^ 31) :
(ofInt n).toInt = n
source
theorem Int64.toInt_ofInt_of_le {n : Int} (hn : -2 ^ 63 ≤ n) (hn' : n < 2 ^ 63) :
(ofInt n).toInt = n
source
theorem ISize.toInt_ofInt_of_le {n : Int} (hn : -2 ^ 31 ≤ n) (hn' : n < 2 ^ 31) :
(ofInt n).toInt = n
source
theorem ISize.toInt_ofInt_of_two_pow_numBits_le {n : Int} (hn : -2 ^ (System.Platform.numBits - 1) ≤ n) (hn' : n < 2 ^ (System.Platform.numBits - 1)) :
(ofInt n).toInt = n
source
theorem ISize.toNatClampNeg_ofInt_eq_zero {n : Int} (hn : -2 ^ 31 ≤ n) (hn' : n ≤ 0) :
(ofInt n).toNatClampNeg = 0
source
theorem Int8.neg_ofInt {n : Int} :
-ofInt n = ofInt (-n)
source
theorem Int16.neg_ofInt {n : Int} :
-ofInt n = ofInt (-n)
source
theorem Int32.neg_ofInt {n : Int} :
-ofInt n = ofInt (-n)
source
theorem Int64.neg_ofInt {n : Int} :
-ofInt n = ofInt (-n)
source
theorem ISize.neg_ofInt {n : Int} :
-ofInt n = ofInt (-n)
source
theorem Int8.ofInt_eq_ofNat {n : Nat} :
ofInt ↑n = ofNat n
source
theorem Int16.ofInt_eq_ofNat {n : Nat} :
ofInt ↑n = ofNat n
source
theorem Int32.ofInt_eq_ofNat {n : Nat} :
ofInt ↑n = ofNat n
source
theorem Int64.ofInt_eq_ofNat {n : Nat} :
ofInt ↑n = ofNat n
source
theorem ISize.ofInt_eq_ofNat {n : Nat} :
ofInt ↑n = ofNat n
source
theorem Int8.neg_ofNat {n : Nat} :
-ofNat n = ofInt (-↑n)
source
theorem Int16.neg_ofNat {n : Nat} :
-ofNat n = ofInt (-↑n)
source
theorem Int32.neg_ofNat {n : Nat} :
-ofNat n = ofInt (-↑n)
source
theorem Int64.neg_ofNat {n : Nat} :
-ofNat n = ofInt (-↑n)
source
theorem ISize.neg_ofNat {n : Nat} :
-ofNat n = ofInt (-↑n)
source
theorem Int8.toNatClampNeg_ofNat_of_lt {n : Nat} (h : n < 2 ^ 7) :
(ofNat n).toNatClampNeg = n
source
theorem Int16.toNatClampNeg_ofNat_of_lt {n : Nat} (h : n < 2 ^ 15) :
(ofNat n).toNatClampNeg = n
source
theorem Int32.toNatClampNeg_ofNat_of_lt {n : Nat} (h : n < 2 ^ 31) :
(ofNat n).toNatClampNeg = n
source
theorem Int64.toNatClampNeg_ofNat_of_lt {n : Nat} (h : n < 2 ^ 63) :
(ofNat n).toNatClampNeg = n
source
theorem ISize.toNatClampNeg_ofNat_of_lt {n : Nat} (h : n < 2 ^ 31) :
(ofNat n).toNatClampNeg = n
source
theorem ISize.toNatClampNeg_ofNat_of_lt_two_pow_numBits {n : Nat} (h : n < 2 ^ (System.Platform.numBits - 1)) :
(ofNat n).toNatClampNeg = n
source
theorem ISize.toNatClampNeg_neg_ofNat_of_le {n : Nat} (h : n ≤ 2 ^ 31) :
(-ofNat n).toNatClampNeg = 0
source
theorem Int8.toInt_ofNat_of_lt {n : Nat} (h : n < 2 ^ 7) :
(ofNat n).toInt = ↑n
source
theorem Int16.toInt_ofNat_of_lt {n : Nat} (h : n < 2 ^ 15) :
(ofNat n).toInt = ↑n
source
theorem Int32.toInt_ofNat_of_lt {n : Nat} (h : n < 2 ^ 31) :
(ofNat n).toInt = ↑n
source
theorem Int64.toInt_ofNat_of_lt {n : Nat} (h : n < 2 ^ 63) :
(ofNat n).toInt = ↑n
source
theorem ISize.toInt_ofNat_of_lt {n : Nat} (h : n < 2 ^ 31) :
(ofNat n).toInt = ↑n
source
theorem ISize.toInt_ofNat_of_lt_two_pow_numBits {n : Nat} (h : n < 2 ^ (System.Platform.numBits - 1)) :
(ofNat n).toInt = ↑n
source
theorem Int64.toInt_neg_ofNat_of_le {n : Nat} (h : n ≤ 2 ^ 63) :
(-ofNat n).toInt = -↑n
source
theorem ISize.toInt_neg_ofNat_of_le {n : Nat} (h : n ≤ 2 ^ 31) :
(-ofNat n).toInt = -↑n
source
theorem Int8.toInt_zero :
toInt 0 = 0
source
theorem Int16.toInt_zero :
toInt 0 = 0
source
theorem Int32.toInt_zero :
toInt 0 = 0
source
theorem Int64.toInt_zero :
toInt 0 = 0
source
theorem ISize.toInt_zero :
toInt 0 = 0
source
theorem Int8.toInt_minValue :
minValue.toInt = -2 ^ 7
source
theorem Int16.toInt_minValue :
minValue.toInt = -2 ^ 15
source
theorem Int32.toInt_minValue :
minValue.toInt = -2 ^ 31
source
theorem Int64.toInt_minValue :
minValue.toInt = -2 ^ 63
source
theorem ISize.toInt_minValue :
minValue.toInt = -2 ^ (System.Platform.numBits - 1)
source
theorem Int8.toInt_maxValue :
maxValue.toInt = 2 ^ 7 - 1
source
theorem Int16.toInt_maxValue :
maxValue.toInt = 2 ^ 15 - 1
source
theorem Int32.toInt_maxValue :
maxValue.toInt = 2 ^ 31 - 1
source
theorem Int64.toInt_maxValue :
maxValue.toInt = 2 ^ 63 - 1
source
theorem ISize.toInt_maxValue :
maxValue.toInt = 2 ^ (System.Platform.numBits - 1) - 1
source
@[simp]
theorem Int8.toNatClampNeg_minValue :
minValue.toNatClampNeg = 0
source
@[simp]
theorem Int16.toNatClampNeg_minValue :
minValue.toNatClampNeg = 0
source
@[simp]
theorem Int32.toNatClampNeg_minValue :
minValue.toNatClampNeg = 0
source
@[simp]
theorem Int64.toNatClampNeg_minValue :
minValue.toNatClampNeg = 0
source
@[simp]
theorem ISize.toNatClampNeg_minValue :
minValue.toNatClampNeg = 0
source
@[simp]
theorem UInt8.toBitVec_toInt8 (x : UInt8) :
x.toInt8.toBitVec = x.toBitVec
source
@[simp]
theorem UInt16.toBitVec_toInt16 (x : UInt16) :
x.toInt16.toBitVec = x.toBitVec
source
@[simp]
theorem UInt32.toBitVec_toInt32 (x : UInt32) :
x.toInt32.toBitVec = x.toBitVec
source
@[simp]
theorem UInt64.toBitVec_toInt64 (x : UInt64) :
x.toInt64.toBitVec = x.toBitVec
source
@[simp]
theorem USize.toBitVec_toISize (x : USize) :
x.toISize.toBitVec = x.toBitVec
source
@[simp]
theorem Int8.ofBitVec_uInt8ToBitVec (x : UInt8) :
ofBitVec x.toBitVec = x.toInt8
source
@[simp]
theorem Int16.ofBitVec_uInt16ToBitVec (x : UInt16) :
ofBitVec x.toBitVec = x.toInt16
source
@[simp]
theorem Int32.ofBitVec_uInt32ToBitVec (x : UInt32) :
ofBitVec x.toBitVec = x.toInt32
source
@[simp]
theorem Int64.ofBitVec_uInt64ToBitVec (x : UInt64) :
ofBitVec x.toBitVec = x.toInt64
source
@[simp]
theorem ISize.ofBitVec_uSizeToBitVec (x : USize) :
ofBitVec x.toBitVec = x.toISize
source
@[simp]
theorem UInt8.toUInt8_toInt8 (x : UInt8) :
x.toInt8.toUInt8 = x
source
@[simp]
theorem UInt16.toUInt16_toInt16 (x : UInt16) :
x.toInt16.toUInt16 = x
source
@[simp]
theorem UInt32.toUInt32_toInt32 (x : UInt32) :
x.toInt32.toUInt32 = x
source
@[simp]
theorem UInt64.toUInt64_toInt64 (x : UInt64) :
x.toInt64.toUInt64 = x
source
@[simp]
theorem USize.toUSize_toISize (x : USize) :
x.toISize.toUSize = x
source
@[simp]
theorem Int8.toNat_toInt (x : Int8) :
x.toInt.toNat = x.toNatClampNeg
source
@[simp]
theorem Int16.toNat_toInt (x : Int16) :
x.toInt.toNat = x.toNatClampNeg
source
@[simp]
theorem Int32.toNat_toInt (x : Int32) :
x.toInt.toNat = x.toNatClampNeg
source
@[simp]
theorem Int64.toNat_toInt (x : Int64) :
x.toInt.toNat = x.toNatClampNeg
source
@[simp]
theorem ISize.toNat_toInt (x : ISize) :
x.toInt.toNat = x.toNatClampNeg
source
@[simp]
theorem Int8.toInt_toBitVec (x : Int8) :
x.toBitVec.toInt = x.toInt
source
@[simp]
theorem Int16.toInt_toBitVec (x : Int16) :
x.toBitVec.toInt = x.toInt
source
@[simp]
theorem Int32.toInt_toBitVec (x : Int32) :
x.toBitVec.toInt = x.toInt
source
@[simp]
theorem Int64.toInt_toBitVec (x : Int64) :
x.toBitVec.toInt = x.toInt
source
@[simp]
theorem ISize.toInt_toBitVec (x : ISize) :
x.toBitVec.toInt = x.toInt
source
@[simp]
theorem Int8.toBitVec_toInt16 (x : Int8) :
x.toInt16.toBitVec = BitVec.signExtend 16 x.toBitVec
source
@[simp]
theorem Int8.toBitVec_toInt32 (x : Int8) :
x.toInt32.toBitVec = BitVec.signExtend 32 x.toBitVec
source
@[simp]
theorem Int8.toBitVec_toInt64 (x : Int8) :
x.toInt64.toBitVec = BitVec.signExtend 64 x.toBitVec
source
@[simp]
theorem Int8.toBitVec_toISize (x : Int8) :
x.toISize.toBitVec = BitVec.signExtend System.Platform.numBits x.toBitVec
source
@[simp]
theorem Int16.toBitVec_toInt8 (x : Int16) :
x.toInt8.toBitVec = BitVec.signExtend 8 x.toBitVec
source
@[simp]
theorem Int16.toBitVec_toInt32 (x : Int16) :
x.toInt32.toBitVec = BitVec.signExtend 32 x.toBitVec
source
@[simp]
theorem Int16.toBitVec_toInt64 (x : Int16) :
x.toInt64.toBitVec = BitVec.signExtend 64 x.toBitVec
source
@[simp]
theorem Int16.toBitVec_toISize (x : Int16) :
x.toISize.toBitVec = BitVec.signExtend System.Platform.numBits x.toBitVec
source
@[simp]
theorem Int32.toBitVec_toInt8 (x : Int32) :
x.toInt8.toBitVec = BitVec.signExtend 8 x.toBitVec
source
@[simp]
theorem Int32.toBitVec_toInt16 (x : Int32) :
x.toInt16.toBitVec = BitVec.signExtend 16 x.toBitVec
source
@[simp]
theorem Int32.toBitVec_toInt64 (x : Int32) :
x.toInt64.toBitVec = BitVec.signExtend 64 x.toBitVec
source
@[simp]
theorem Int32.toBitVec_toISize (x : Int32) :
x.toISize.toBitVec = BitVec.signExtend System.Platform.numBits x.toBitVec
source
@[simp]
theorem Int64.toBitVec_toInt8 (x : Int64) :
x.toInt8.toBitVec = BitVec.signExtend 8 x.toBitVec
source
@[simp]
theorem Int64.toBitVec_toInt16 (x : Int64) :
x.toInt16.toBitVec = BitVec.signExtend 16 x.toBitVec
source
@[simp]
theorem Int64.toBitVec_toInt32 (x : Int64) :
x.toInt32.toBitVec = BitVec.signExtend 32 x.toBitVec
source
@[simp]
theorem Int64.toBitVec_toISize (x : Int64) :
x.toISize.toBitVec = BitVec.signExtend System.Platform.numBits x.toBitVec
source
@[simp]
theorem ISize.toBitVec_toInt8 (x : ISize) :
x.toInt8.toBitVec = BitVec.signExtend 8 x.toBitVec
source
@[simp]
theorem ISize.toBitVec_toInt16 (x : ISize) :
x.toInt16.toBitVec = BitVec.signExtend 16 x.toBitVec
source
@[simp]
theorem ISize.toBitVec_toInt32 (x : ISize) :
x.toInt32.toBitVec = BitVec.signExtend 32 x.toBitVec
source
@[simp]
theorem ISize.toBitVec_toInt64 (x : ISize) :
x.toInt64.toBitVec = BitVec.signExtend 64 x.toBitVec
source
theorem Int8.toInt_lt (x : Int8) :
x.toInt < 2 ^ 7
source
theorem Int8.le_toInt (x : Int8) :
-2 ^ 7 ≤ x.toInt
source
theorem Int16.toInt_lt (x : Int16) :
x.toInt < 2 ^ 15
source
theorem Int16.le_toInt (x : Int16) :
-2 ^ 15 ≤ x.toInt
source
theorem Int32.toInt_lt (x : Int32) :
x.toInt < 2 ^ 31
source
theorem Int32.le_toInt (x : Int32) :
-2 ^ 31 ≤ x.toInt
source
theorem Int64.toInt_lt (x : Int64) :
x.toInt < 2 ^ 63
source
theorem Int64.le_toInt (x : Int64) :
-2 ^ 63 ≤ x.toInt
source
theorem ISize.toInt_lt_two_pow_numBits (x : ISize) :
x.toInt < 2 ^ (System.Platform.numBits - 1)
source
theorem ISize.two_pow_numBits_le_toInt (x : ISize) :
-2 ^ (System.Platform.numBits - 1) ≤ x.toInt
source
theorem ISize.toInt_lt (x : ISize) :
x.toInt < 2 ^ 63
source
theorem ISize.le_toInt (x : ISize) :
-2 ^ 63 ≤ x.toInt
source
theorem Int8.toInt_le (x : Int8) :
x.toInt ≤ maxValue.toInt
source
theorem Int16.toInt_le (x : Int16) :
x.toInt ≤ maxValue.toInt
source
theorem Int32.toInt_le (x : Int32) :
x.toInt ≤ maxValue.toInt
source
theorem Int64.toInt_le (x : Int64) :
x.toInt ≤ maxValue.toInt
source
theorem ISize.toInt_le (x : ISize) :
x.toInt ≤ maxValue.toInt
source
theorem Int8.minValue_le_toInt (x : Int8) :
minValue.toInt ≤ x.toInt
source
theorem Int16.minValue_le_toInt (x : Int16) :
minValue.toInt ≤ x.toInt
source
theorem Int32.minValue_le_toInt (x : Int32) :
minValue.toInt ≤ x.toInt
source
theorem Int64.minValue_le_toInt (x : Int64) :
minValue.toInt ≤ x.toInt
source
theorem ISize.minValue_le_toInt (x : ISize) :
minValue.toInt ≤ x.toInt
source
theorem ISize.toInt_minValue_le :
minValue.toInt ≤ -2 ^ 31
source
theorem ISize.le_toInt_maxValue :
2 ^ 31 - 1 ≤ maxValue.toInt
source
theorem Int8.iSizeMinValue_le_toInt (x : Int8) :
ISize.minValue.toInt ≤ x.toInt
source
theorem Int8.toInt_le_iSizeMaxValue (x : Int8) :
x.toInt ≤ ISize.maxValue.toInt
source
theorem Int16.iSizeMinValue_le_toInt (x : Int16) :
ISize.minValue.toInt ≤ x.toInt
source
theorem Int16.toInt_le_iSizeMaxValue (x : Int16) :
x.toInt ≤ ISize.maxValue.toInt
source
theorem Int32.iSizeMinValue_le_toInt (x : Int32) :
ISize.minValue.toInt ≤ x.toInt
source
theorem Int32.toInt_le_iSizeMaxValue (x : Int32) :
x.toInt ≤ ISize.maxValue.toInt
source
theorem ISize.int64MinValue_le_toInt (x : ISize) :
Int64.minValue.toInt ≤ x.toInt
source
theorem ISize.toInt_le_int64MaxValue (x : ISize) :
x.toInt ≤ Int64.maxValue.toInt
source
theorem Int8.toNatClampNeg_lt (x : Int8) :
x.toNatClampNeg < 2 ^ 7
source
theorem Int16.toNatClampNeg_lt (x : Int16) :
x.toNatClampNeg < 2 ^ 15
source
theorem Int32.toNatClampNeg_lt (x : Int32) :
x.toNatClampNeg < 2 ^ 31
source
theorem Int64.toNatClampNeg_lt (x : Int64) :
x.toNatClampNeg < 2 ^ 63
source
theorem ISize.toNatClampNeg_lt_two_pow_numBits (x : ISize) :
x.toNatClampNeg < 2 ^ (System.Platform.numBits - 1)
source
theorem ISize.toNatClampNeg_lt (x : ISize) :
x.toNatClampNeg < 2 ^ 63
source
@[simp]
theorem Int8.toInt_toInt16 (x : Int8) :
x.toInt16.toInt = x.toInt
source
@[simp]
theorem Int8.toInt_toInt32 (x : Int8) :
x.toInt32.toInt = x.toInt
source
@[simp]
theorem Int8.toInt_toInt64 (x : Int8) :
x.toInt64.toInt = x.toInt
source
@[simp]
theorem Int8.toInt_toISize (x : Int8) :
x.toISize.toInt = x.toInt
source
@[simp]
theorem Int16.toInt_toInt8 (x : Int16) :
x.toInt8.toInt = x.toInt.bmod (2 ^ 8)
source
@[simp]
theorem Int16.toInt_toInt32 (x : Int16) :
x.toInt32.toInt = x.toInt
source
@[simp]
theorem Int16.toInt_toInt64 (x : Int16) :
x.toInt64.toInt = x.toInt
source
@[simp]
theorem Int16.toInt_toISize (x : Int16) :
x.toISize.toInt = x.toInt
source
@[simp]
theorem Int32.toInt_toInt8 (x : Int32) :
x.toInt8.toInt = x.toInt.bmod (2 ^ 8)
source
@[simp]
theorem Int32.toInt_toInt16 (x : Int32) :
x.toInt16.toInt = x.toInt.bmod (2 ^ 16)
source
@[simp]
theorem Int32.toInt_toInt64 (x : Int32) :
x.toInt64.toInt = x.toInt
source
@[simp]
theorem Int32.toInt_toISize (x : Int32) :
x.toISize.toInt = x.toInt
source
@[simp]
theorem Int64.toInt_toInt8 (x : Int64) :
x.toInt8.toInt = x.toInt.bmod (2 ^ 8)
source
@[simp]
theorem Int64.toInt_toInt16 (x : Int64) :
x.toInt16.toInt = x.toInt.bmod (2 ^ 16)
source
@[simp]
theorem Int64.toInt_toInt32 (x : Int64) :
x.toInt32.toInt = x.toInt.bmod (2 ^ 32)
source
@[simp]
theorem Int64.toInt_toISize (x : Int64) :
x.toISize.toInt = x.toInt.bmod (2 ^ System.Platform.numBits)
source
@[simp]
theorem ISize.toInt_toInt8 (x : ISize) :
x.toInt8.toInt = x.toInt.bmod (2 ^ 8)
source
@[simp]
theorem ISize.toInt_toInt16 (x : ISize) :
x.toInt16.toInt = x.toInt.bmod (2 ^ 16)
source
@[simp]
theorem ISize.toInt_toInt32 (x : ISize) :
x.toInt32.toInt = x.toInt.bmod (2 ^ 32)
source
@[simp]
theorem ISize.toInt_toInt64 (x : ISize) :
x.toInt64.toInt = x.toInt
source
@[simp]
theorem Int8.toNatClampNeg_toInt16 (x : Int8) :
x.toInt16.toNatClampNeg = x.toNatClampNeg
source
@[simp]
theorem Int8.toNatClampNeg_toInt32 (x : Int8) :
x.toInt32.toNatClampNeg = x.toNatClampNeg
source
@[simp]
theorem Int8.toNatClampNeg_toInt64 (x : Int8) :
x.toInt64.toNatClampNeg = x.toNatClampNeg
source
@[simp]
theorem Int8.toNatClampNeg_toISize (x : Int8) :
x.toISize.toNatClampNeg = x.toNatClampNeg
source
@[simp]
theorem Int16.toNatClampNeg_toInt32 (x : Int16) :
x.toInt32.toNatClampNeg = x.toNatClampNeg
source
@[simp]
theorem Int16.toNatClampNeg_toInt64 (x : Int16) :
x.toInt64.toNatClampNeg = x.toNatClampNeg
source
@[simp]
theorem Int16.toNatClampNeg_toISize (x : Int16) :
x.toISize.toNatClampNeg = x.toNatClampNeg
source
@[simp]
theorem Int32.toNatClampNeg_toInt64 (x : Int32) :
x.toInt64.toNatClampNeg = x.toNatClampNeg
source
@[simp]
theorem Int32.toNatClampNeg_toISize (x : Int32) :
x.toISize.toNatClampNeg = x.toNatClampNeg
source
@[simp]
theorem ISize.toNatClampNeg_toInt64 (x : ISize) :
x.toInt64.toNatClampNeg = x.toNatClampNeg
source
@[simp]
theorem Int8.toInt8_toUInt8 (x : Int8) :
x.toUInt8.toInt8 = x
source
@[simp]
theorem Int16.toInt16_toUInt16 (x : Int16) :
x.toUInt16.toInt16 = x
source
@[simp]
theorem Int32.toInt32_toUInt32 (x : Int32) :
x.toUInt32.toInt32 = x
source
@[simp]
theorem Int64.toInt64_toUInt64 (x : Int64) :
x.toUInt64.toInt64 = x
source
@[simp]
theorem ISize.toISize_toUSize (x : ISize) :
x.toUSize.toISize = x
source
theorem Int8.toNat_toBitVec (x : Int8) :
x.toBitVec.toNat = x.toUInt8.toNat
source
theorem Int16.toNat_toBitVec (x : Int16) :
x.toBitVec.toNat = x.toUInt16.toNat
source
theorem Int32.toNat_toBitVec (x : Int32) :
x.toBitVec.toNat = x.toUInt32.toNat
source
theorem Int64.toNat_toBitVec (x : Int64) :
x.toBitVec.toNat = x.toUInt64.toNat
source
theorem ISize.toNat_toBitVec (x : ISize) :
x.toBitVec.toNat = x.toUSize.toNat
source
theorem Int8.toNat_toBitVec_of_le {x : Int8} (hx : 0 ≤ x) :
x.toBitVec.toNat = x.toNatClampNeg
source
theorem Int16.toNat_toBitVec_of_le {x : Int16} (hx : 0 ≤ x) :
x.toBitVec.toNat = x.toNatClampNeg
source
theorem Int32.toNat_toBitVec_of_le {x : Int32} (hx : 0 ≤ x) :
x.toBitVec.toNat = x.toNatClampNeg
source
theorem Int64.toNat_toBitVec_of_le {x : Int64} (hx : 0 ≤ x) :
x.toBitVec.toNat = x.toNatClampNeg
source
theorem ISize.toNat_toBitVec_of_le {x : ISize} (hx : 0 ≤ x) :
x.toBitVec.toNat = x.toNatClampNeg
source
theorem Int8.toNat_toUInt8_of_le {x : Int8} (hx : 0 ≤ x) :
x.toUInt8.toNat = x.toNatClampNeg
source
theorem Int16.toNat_toUInt16_of_le {x : Int16} (hx : 0 ≤ x) :
x.toUInt16.toNat = x.toNatClampNeg
source
theorem Int32.toNat_toUInt32_of_le {x : Int32} (hx : 0 ≤ x) :
x.toUInt32.toNat = x.toNatClampNeg
source
theorem Int64.toNat_toUInt64_of_le {x : Int64} (hx : 0 ≤ x) :
x.toUInt64.toNat = x.toNatClampNeg
source
theorem ISize.toNat_toUSize_of_le {x : ISize} (hx : 0 ≤ x) :
x.toUSize.toNat = x.toNatClampNeg
source
theorem Int8.toFin_toBitVec (x : Int8) :
x.toBitVec.toFin = x.toUInt8.toFin
source
theorem Int16.toFin_toBitVec (x : Int16) :
x.toBitVec.toFin = x.toUInt16.toFin
source
theorem Int32.toFin_toBitVec (x : Int32) :
x.toBitVec.toFin = x.toUInt32.toFin
source
theorem Int64.toFin_toBitVec (x : Int64) :
x.toBitVec.toFin = x.toUInt64.toFin
source
theorem ISize.toFin_toBitVec (x : ISize) :
x.toBitVec.toFin = x.toUSize.toFin
source
@[simp]
theorem Int8.toBitVec_toUInt8 (x : Int8) :
x.toUInt8.toBitVec = x.toBitVec
source
@[simp]
theorem Int16.toBitVec_toUInt16 (x : Int16) :
x.toUInt16.toBitVec = x.toBitVec
source
@[simp]
theorem Int32.toBitVec_toUInt32 (x : Int32) :
x.toUInt32.toBitVec = x.toBitVec
source
@[simp]
theorem Int64.toBitVec_toUInt64 (x : Int64) :
x.toUInt64.toBitVec = x.toBitVec
source
@[simp]
theorem ISize.toBitVec_toUSize (x : ISize) :
x.toUSize.toBitVec = x.toBitVec
source
@[simp]
theorem UInt8.ofBitVec_int8ToBitVec (x : Int8) :
{ toBitVec := x.toBitVec } = x.toUInt8
source
@[simp]
theorem UInt16.ofBitVec_int16ToBitVec (x : Int16) :
{ toBitVec := x.toBitVec } = x.toUInt16
source
@[simp]
theorem UInt32.ofBitVec_int32ToBitVec (x : Int32) :
{ toBitVec := x.toBitVec } = x.toUInt32
source
@[simp]
theorem UInt64.ofBitVec_int64ToBitVec (x : Int64) :
{ toBitVec := x.toBitVec } = x.toUInt64
source
@[simp]
theorem USize.ofBitVec_iSizeToBitVec (x : ISize) :
{ toBitVec := x.toBitVec } = x.toUSize
source
@[simp]
theorem Int8.ofBitVec_toBitVec (x : Int8) :
ofBitVec x.toBitVec = x
source
@[simp]
theorem Int16.ofBitVec_toBitVec (x : Int16) :
ofBitVec x.toBitVec = x
source
@[simp]
theorem Int32.ofBitVec_toBitVec (x : Int32) :
ofBitVec x.toBitVec = x
source
@[simp]
theorem Int64.ofBitVec_toBitVec (x : Int64) :
ofBitVec x.toBitVec = x
source
@[simp]
theorem ISize.ofBitVec_toBitVec (x : ISize) :
ofBitVec x.toBitVec = x
source
@[simp]
theorem Int8.ofBitVec_int16ToBitVec (x : Int16) :
ofBitVec (BitVec.signExtend 8 x.toBitVec) = x.toInt8
source
@[simp]
theorem Int8.ofBitVec_int32ToBitVec (x : Int32) :
ofBitVec (BitVec.signExtend 8 x.toBitVec) = x.toInt8
source
@[simp]
theorem Int8.ofBitVec_int64ToBitVec (x : Int64) :
ofBitVec (BitVec.signExtend 8 x.toBitVec) = x.toInt8
source
@[simp]
theorem Int8.ofBitVec_iSizeToBitVec (x : ISize) :
ofBitVec (BitVec.signExtend 8 x.toBitVec) = x.toInt8
source
@[simp]
theorem Int16.ofBitVec_int8ToBitVec (x : Int8) :
ofBitVec (BitVec.signExtend 16 x.toBitVec) = x.toInt16
source
@[simp]
theorem Int16.ofBitVec_int32ToBitVec (x : Int32) :
ofBitVec (BitVec.signExtend 16 x.toBitVec) = x.toInt16
source
@[simp]
theorem Int16.ofBitVec_int64ToBitVec (x : Int64) :
ofBitVec (BitVec.signExtend 16 x.toBitVec) = x.toInt16
source
@[simp]
theorem Int16.ofBitVec_iSizeToBitVec (x : ISize) :
ofBitVec (BitVec.signExtend 16 x.toBitVec) = x.toInt16
source
@[simp]
theorem Int32.ofBitVec_int8ToBitVec (x : Int8) :
ofBitVec (BitVec.signExtend 32 x.toBitVec) = x.toInt32
source
@[simp]
theorem Int32.ofBitVec_int16ToBitVec (x : Int16) :
ofBitVec (BitVec.signExtend 32 x.toBitVec) = x.toInt32
source
@[simp]
theorem Int32.ofBitVec_int64ToBitVec (x : Int64) :
ofBitVec (BitVec.signExtend 32 x.toBitVec) = x.toInt32
source
@[simp]
theorem Int32.ofBitVec_iSizeToBitVec (x : ISize) :
ofBitVec (BitVec.signExtend 32 x.toBitVec) = x.toInt32
source
@[simp]
theorem Int64.ofBitVec_int8ToBitVec (x : Int8) :
ofBitVec (BitVec.signExtend 64 x.toBitVec) = x.toInt64
source
@[simp]
theorem Int64.ofBitVec_int16ToBitVec (x : Int16) :
ofBitVec (BitVec.signExtend 64 x.toBitVec) = x.toInt64
source
@[simp]
theorem Int64.ofBitVec_int32ToBitVec (x : Int32) :
ofBitVec (BitVec.signExtend 64 x.toBitVec) = x.toInt64
source
@[simp]
theorem Int64.ofBitVec_iSizeToBitVec (x : ISize) :
ofBitVec (BitVec.signExtend 64 x.toBitVec) = x.toInt64
source
@[simp]
theorem ISize.ofBitVec_int8ToBitVec (x : Int8) :
ofBitVec (BitVec.signExtend System.Platform.numBits x.toBitVec) = x.toISize
source
@[simp]
theorem ISize.ofBitVec_int16ToBitVec (x : Int16) :
ofBitVec (BitVec.signExtend System.Platform.numBits x.toBitVec) = x.toISize
source
@[simp]
theorem ISize.ofBitVec_int32ToBitVec (x : Int32) :
ofBitVec (BitVec.signExtend System.Platform.numBits x.toBitVec) = x.toISize
source
@[simp]
theorem ISize.ofBitVec_int64ToBitVec (x : Int64) :
ofBitVec (BitVec.signExtend System.Platform.numBits x.toBitVec) = x.toISize
source
@[simp]
theorem Int8.toBitVec_ofIntLE (x : Int) (h₁ : minValue.toInt ≤ x) (h₂ : x ≤ maxValue.toInt) :
(ofIntLE x h₁ h₂).toBitVec = BitVec.ofInt 8 x
source
@[simp]
theorem Int16.toBitVec_ofIntLE (x : Int) (h₁ : minValue.toInt ≤ x) (h₂ : x ≤ maxValue.toInt) :
(ofIntLE x h₁ h₂).toBitVec = BitVec.ofInt 16 x
source
@[simp]
theorem Int32.toBitVec_ofIntLE (x : Int) (h₁ : minValue.toInt ≤ x) (h₂ : x ≤ maxValue.toInt) :
(ofIntLE x h₁ h₂).toBitVec = BitVec.ofInt 32 x
source
@[simp]
theorem Int64.toBitVec_ofIntLE (x : Int) (h₁ : minValue.toInt ≤ x) (h₂ : x ≤ maxValue.toInt) :
(ofIntLE x h₁ h₂).toBitVec = BitVec.ofInt 64 x
source
@[simp]
theorem ISize.toBitVec_ofIntLE (x : Int) (h₁ : minValue.toInt ≤ x) (h₂ : x ≤ maxValue.toInt) :
(ofIntLE x h₁ h₂).toBitVec = BitVec.ofInt System.Platform.numBits x
source
@[simp]
theorem Int8.toInt_bmod (x : Int8) :
x.toInt.bmod 256 = x.toInt
source
@[simp]
theorem Int16.toInt_bmod (x : Int16) :
x.toInt.bmod 65536 = x.toInt
source
@[simp]
theorem Int32.toInt_bmod (x : Int32) :
x.toInt.bmod 4294967296 = x.toInt
source
@[simp]
theorem Int64.toInt_bmod (x : Int64) :
x.toInt.bmod 18446744073709551616 = x.toInt
source
@[simp]
theorem ISize.toInt_bmod_two_pow_numBits (x : ISize) :
x.toInt.bmod (2 ^ System.Platform.numBits) = x.toInt
source
@[simp]
theorem Int8.toInt_bmod_65536 (x : Int8) :
x.toInt.bmod 65536 = x.toInt
source
@[simp]
theorem Int8.toInt_bmod_4294967296 (x : Int8) :
x.toInt.bmod 4294967296 = x.toInt
source
@[simp]
theorem Int16.toInt_bmod_4294967296 (x : Int16) :
x.toInt.bmod 4294967296 = x.toInt
source
@[simp]
theorem Int8.toInt_bmod_18446744073709551616 (x : Int8) :
x.toInt.bmod 18446744073709551616 = x.toInt
source
@[simp]
theorem Int16.toInt_bmod_18446744073709551616 (x : Int16) :
x.toInt.bmod 18446744073709551616 = x.toInt
source
@[simp]
theorem Int32.toInt_bmod_18446744073709551616 (x : Int32) :
x.toInt.bmod 18446744073709551616 = x.toInt
source
@[simp]
theorem ISize.toInt_bmod_18446744073709551616 (x : ISize) :
x.toInt.bmod 18446744073709551616 = x.toInt
source
@[simp]
theorem Int8.toInt_bmod_two_pow_numBits (x : Int8) :
x.toInt.bmod (2 ^ System.Platform.numBits) = x.toInt
source
@[simp]
theorem Int16.toInt_bmod_two_pow_numBits (x : Int16) :
x.toInt.bmod (2 ^ System.Platform.numBits) = x.toInt
source
@[simp]
theorem Int32.toInt_bmod_two_pow_numBits (x : Int32) :
x.toInt.bmod (2 ^ System.Platform.numBits) = x.toInt
source
@[simp]
theorem BitVec.ofInt_int8ToInt (x : Int8) :
BitVec.ofInt 8 x.toInt = x.toBitVec
source
@[simp]
theorem BitVec.ofInt_int16ToInt (x : Int16) :
BitVec.ofInt 16 x.toInt = x.toBitVec
source
@[simp]
theorem BitVec.ofInt_int32ToInt (x : Int32) :
BitVec.ofInt 32 x.toInt = x.toBitVec
source
@[simp]
theorem BitVec.ofInt_int64ToInt (x : Int64) :
BitVec.ofInt 64 x.toInt = x.toBitVec
source
@[simp]
theorem BitVec.ofInt_iSizeToInt (x : ISize) :
BitVec.ofInt System.Platform.numBits x.toInt = x.toBitVec
source
@[simp]
theorem Int8.ofIntLE_toInt (x : Int8) :
ofIntLE x.toInt ⋯ ⋯ = x
source
@[simp]
theorem Int16.ofIntLE_toInt (x : Int16) :
ofIntLE x.toInt ⋯ ⋯ = x
source
@[simp]
theorem Int32.ofIntLE_toInt (x : Int32) :
ofIntLE x.toInt ⋯ ⋯ = x
source
@[simp]
theorem Int64.ofIntLE_toInt (x : Int64) :
ofIntLE x.toInt ⋯ ⋯ = x
source
@[simp]
theorem ISize.ofIntLE_toInt (x : ISize) :
ofIntLE x.toInt ⋯ ⋯ = x
source
theorem Int8.ofIntLE_int16ToInt (x : Int16) {h₁ : minValue.toInt ≤ x.toInt} {h₂ : x.toInt ≤ maxValue.toInt} :
ofIntLE x.toInt h₁ h₂ = x.toInt8
source
theorem Int8.ofIntLE_int32ToInt (x : Int32) {h₁ : minValue.toInt ≤ x.toInt} {h₂ : x.toInt ≤ maxValue.toInt} :
ofIntLE x.toInt h₁ h₂ = x.toInt8
source
theorem Int8.ofIntLE_int64ToInt (x : Int64) {h₁ : minValue.toInt ≤ x.toInt} {h₂ : x.toInt ≤ maxValue.toInt} :
ofIntLE x.toInt h₁ h₂ = x.toInt8
source
theorem Int8.ofIntLE_iSizeToInt (x : ISize) {h₁ : minValue.toInt ≤ x.toInt} {h₂ : x.toInt ≤ maxValue.toInt} :
ofIntLE x.toInt h₁ h₂ = x.toInt8
source
@[simp]
theorem Int16.ofIntLE_int8ToInt (x : Int8) :
ofIntLE x.toInt ⋯ ⋯ = x.toInt16
source
theorem Int16.ofIntLE_int32ToInt (x : Int32) {h₁ : minValue.toInt ≤ x.toInt} {h₂ : x.toInt ≤ maxValue.toInt} :
ofIntLE x.toInt h₁ h₂ = x.toInt16
source
theorem Int16.ofIntLE_int64ToInt (x : Int64) {h₁ : minValue.toInt ≤ x.toInt} {h₂ : x.toInt ≤ maxValue.toInt} :
ofIntLE x.toInt h₁ h₂ = x.toInt16
source
theorem Int16.ofIntLE_iSizeToInt (x : ISize) {h₁ : minValue.toInt ≤ x.toInt} {h₂ : x.toInt ≤ maxValue.toInt} :
ofIntLE x.toInt h₁ h₂ = x.toInt16
source
@[simp]
theorem Int32.ofIntLE_int8ToInt (x : Int8) :
ofIntLE x.toInt ⋯ ⋯ = x.toInt32
source
@[simp]
theorem Int32.ofIntLE_int16ToInt (x : Int16) :
ofIntLE x.toInt ⋯ ⋯ = x.toInt32
source
theorem Int32.ofIntLE_int64ToInt (x : Int64) {h₁ : minValue.toInt ≤ x.toInt} {h₂ : x.toInt ≤ maxValue.toInt} :
ofIntLE x.toInt h₁ h₂ = x.toInt32
source
theorem Int32.ofIntLE_iSizeToInt (x : ISize) {h₁ : minValue.toInt ≤ x.toInt} {h₂ : x.toInt ≤ maxValue.toInt} :
ofIntLE x.toInt h₁ h₂ = x.toInt32
source
@[simp]
theorem Int64.ofIntLE_int8ToInt (x : Int8) :
ofIntLE x.toInt ⋯ ⋯ = x.toInt64
source
@[simp]
theorem Int64.ofIntLE_int16ToInt (x : Int16) :
ofIntLE x.toInt ⋯ ⋯ = x.toInt64
source
@[simp]
theorem Int64.ofIntLE_int32ToInt (x : Int32) :
ofIntLE x.toInt ⋯ ⋯ = x.toInt64
source
@[simp]
theorem Int64.ofIntLE_iSizeToInt (x : ISize) :
ofIntLE x.toInt ⋯ ⋯ = x.toInt64
source
@[simp]
theorem ISize.ofIntLE_int8ToInt (x : Int8) :
ofIntLE x.toInt ⋯ ⋯ = x.toISize
source
@[simp]
theorem ISize.ofIntLE_int16ToInt (x : Int16) :
ofIntLE x.toInt ⋯ ⋯ = x.toISize
source
@[simp]
theorem ISize.ofIntLE_int32ToInt (x : Int32) :
ofIntLE x.toInt ⋯ ⋯ = x.toISize
source
theorem ISize.ofIntLE_int64ToInt (x : Int64) {h₁ : minValue.toInt ≤ x.toInt} {h₂ : x.toInt ≤ maxValue.toInt} :
ofIntLE x.toInt h₁ h₂ = x.toISize
source
@[simp]
theorem Int8.ofInt_toInt (x : Int8) :
ofInt x.toInt = x
source
@[simp]
theorem Int16.ofInt_toInt (x : Int16) :
ofInt x.toInt = x
source
@[simp]
theorem Int32.ofInt_toInt (x : Int32) :
ofInt x.toInt = x
source
@[simp]
theorem Int64.ofInt_toInt (x : Int64) :
ofInt x.toInt = x
source
@[simp]
theorem ISize.ofInt_toInt (x : ISize) :
ofInt x.toInt = x
source
@[simp]
theorem Int8.ofInt_int16ToInt (x : Int16) :
ofInt x.toInt = x.toInt8
source
@[simp]
theorem Int8.ofInt_int32ToInt (x : Int32) :
ofInt x.toInt = x.toInt8
source
@[simp]
theorem Int8.ofInt_int64ToInt (x : Int64) :
ofInt x.toInt = x.toInt8
source
@[simp]
theorem Int8.ofInt_iSizeToInt (x : ISize) :
ofInt x.toInt = x.toInt8
source
@[simp]
theorem Int16.ofInt_int8ToInt (x : Int8) :
ofInt x.toInt = x.toInt16
source
@[simp]
theorem Int16.ofInt_int32ToInt (x : Int32) :
ofInt x.toInt = x.toInt16
source
@[simp]
theorem Int16.ofInt_int64ToInt (x : Int64) :
ofInt x.toInt = x.toInt16
source
@[simp]
theorem Int16.ofInt_iSizeToInt (x : ISize) :
ofInt x.toInt = x.toInt16
source
@[simp]
theorem Int32.ofInt_int8ToInt (x : Int8) :
ofInt x.toInt = x.toInt32
source
@[simp]
theorem Int32.ofInt_int16ToInt (x : Int16) :
ofInt x.toInt = x.toInt32
source
@[simp]
theorem Int32.ofInt_int64ToInt (x : Int64) :
ofInt x.toInt = x.toInt32
source
@[simp]
theorem Int32.ofInt_iSizeToInt (x : ISize) :
ofInt x.toInt = x.toInt32
source
@[simp]
theorem Int64.ofInt_int8ToInt (x : Int8) :
ofInt x.toInt = x.toInt64
source
@[simp]
theorem Int64.ofInt_int16ToInt (x : Int16) :
ofInt x.toInt = x.toInt64
source
@[simp]
theorem Int64.ofInt_int32ToInt (x : Int32) :
ofInt x.toInt = x.toInt64
source
@[simp]
theorem Int64.ofInt_iSizeToInt (x : ISize) :
ofInt x.toInt = x.toInt64
source
@[simp]
theorem ISize.ofInt_int8ToInt (x : Int8) :
ofInt x.toInt = x.toISize
source
@[simp]
theorem ISize.ofInt_int16ToInt (x : Int16) :
ofInt x.toInt = x.toISize
source
@[simp]
theorem ISize.ofInt_int32ToInt (x : Int32) :
ofInt x.toInt = x.toISize
source
@[simp]
theorem ISize.ofInt_int64ToInt (x : Int64) :
ofInt x.toInt = x.toISize
source
@[simp]
theorem Int8.toInt_ofIntLE {x : Int} {h₁ : minValue.toInt ≤ x} {h₂ : x ≤ maxValue.toInt} :
(ofIntLE x h₁ h₂).toInt = x
source
@[simp]
theorem Int16.toInt_ofIntLE {x : Int} {h₁ : minValue.toInt ≤ x} {h₂ : x ≤ maxValue.toInt} :
(ofIntLE x h₁ h₂).toInt = x
source
@[simp]
theorem Int32.toInt_ofIntLE {x : Int} {h₁ : minValue.toInt ≤ x} {h₂ : x ≤ maxValue.toInt} :
(ofIntLE x h₁ h₂).toInt = x
source
@[simp]
theorem Int64.toInt_ofIntLE {x : Int} {h₁ : minValue.toInt ≤ x} {h₂ : x ≤ maxValue.toInt} :
(ofIntLE x h₁ h₂).toInt = x
source
@[simp]
theorem ISize.toInt_ofIntLE {x : Int} {h₁ : minValue.toInt ≤ x} {h₂ : x ≤ maxValue.toInt} :
(ofIntLE x h₁ h₂).toInt = x
source
theorem Int8.ofIntLE_eq_ofIntTruncate {x : Int} {h₁ : minValue.toInt ≤ x} {h₂ : x ≤ maxValue.toInt} :
ofIntLE x h₁ h₂ = ofIntTruncate x
source
theorem Int16.ofIntLE_eq_ofIntTruncate {x : Int} {h₁ : minValue.toInt ≤ x} {h₂ : x ≤ maxValue.toInt} :
ofIntLE x h₁ h₂ = ofIntTruncate x
source
theorem Int32.ofIntLE_eq_ofIntTruncate {x : Int} {h₁ : minValue.toInt ≤ x} {h₂ : x ≤ maxValue.toInt} :
ofIntLE x h₁ h₂ = ofIntTruncate x
source
theorem Int64.ofIntLE_eq_ofIntTruncate {x : Int} {h₁ : minValue.toInt ≤ x} {h₂ : x ≤ maxValue.toInt} :
ofIntLE x h₁ h₂ = ofIntTruncate x
source
theorem ISize.ofIntLE_eq_ofIntTruncate {x : Int} {h₁ : minValue.toInt ≤ x} {h₂ : x ≤ maxValue.toInt} :
ofIntLE x h₁ h₂ = ofIntTruncate x
source
theorem Int8.ofIntLE_eq_ofInt {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) :
ofIntLE n h₁ h₂ = ofInt n
source
theorem Int16.ofIntLE_eq_ofInt {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) :
ofIntLE n h₁ h₂ = ofInt n
source
theorem Int32.ofIntLE_eq_ofInt {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) :
ofIntLE n h₁ h₂ = ofInt n
source
theorem Int64.ofIntLE_eq_ofInt {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) :
ofIntLE n h₁ h₂ = ofInt n
source
theorem ISize.ofIntLE_eq_ofInt {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) :
ofIntLE n h₁ h₂ = ofInt n
source
theorem Int8.toInt_ofIntTruncate {x : Int} (h₁ : minValue.toInt ≤ x) (h₂ : x ≤ maxValue.toInt) :
(ofIntTruncate x).toInt = x
source
theorem Int16.toInt_ofIntTruncate {x : Int} (h₁ : minValue.toInt ≤ x) (h₂ : x ≤ maxValue.toInt) :
(ofIntTruncate x).toInt = x
source
theorem Int32.toInt_ofIntTruncate {x : Int} (h₁ : minValue.toInt ≤ x) (h₂ : x ≤ maxValue.toInt) :
(ofIntTruncate x).toInt = x
source
theorem Int64.toInt_ofIntTruncate {x : Int} (h₁ : minValue.toInt ≤ x) (h₂ : x ≤ maxValue.toInt) :
(ofIntTruncate x).toInt = x
source
theorem ISize.toInt_ofIntTruncate {x : Int} (h₁ : minValue.toInt ≤ x) (h₂ : x ≤ maxValue.toInt) :
(ofIntTruncate x).toInt = x
source
@[simp]
theorem Int8.ofIntTruncate_toInt (x : Int8) :
ofIntTruncate x.toInt = x
source
@[simp]
theorem Int16.ofIntTruncate_toInt (x : Int16) :
ofIntTruncate x.toInt = x
source
@[simp]
theorem Int32.ofIntTruncate_toInt (x : Int32) :
ofIntTruncate x.toInt = x
source
@[simp]
theorem Int64.ofIntTruncate_toInt (x : Int64) :
ofIntTruncate x.toInt = x
source
@[simp]
theorem ISize.ofIntTruncate_toInt (x : ISize) :
ofIntTruncate x.toInt = x
source
@[simp]
theorem Int16.ofIntTruncate_int8ToInt (x : Int8) :
ofIntTruncate x.toInt = x.toInt16
source
@[simp]
theorem Int32.ofIntTruncate_int8ToInt (x : Int8) :
ofIntTruncate x.toInt = x.toInt32
source
@[simp]
theorem Int64.ofIntTruncate_int8ToInt (x : Int8) :
ofIntTruncate x.toInt = x.toInt64
source
@[simp]
theorem ISize.ofIntTruncate_int8ToInt (x : Int8) :
ofIntTruncate x.toInt = x.toISize
source
@[simp]
theorem Int32.ofIntTruncate_int16ToInt (x : Int16) :
ofIntTruncate x.toInt = x.toInt32
source
@[simp]
theorem Int64.ofIntTruncate_int16ToInt (x : Int16) :
ofIntTruncate x.toInt = x.toInt64
source
@[simp]
theorem ISize.ofIntTruncate_int16ToInt (x : Int16) :
ofIntTruncate x.toInt = x.toISize
source
@[simp]
theorem Int64.ofIntTruncate_int32ToInt (x : Int32) :
ofIntTruncate x.toInt = x.toInt64
source
@[simp]
theorem ISize.ofIntTruncate_int32ToInt (x : Int32) :
ofIntTruncate x.toInt = x.toISize
source
@[simp]
theorem Int64.ofIntTruncate_iSizeToInt (x : ISize) :
ofIntTruncate x.toInt = x.toInt64
source
theorem Int8.le_iff_toInt_le {x y : Int8} :
x ≤ y ↔ x.toInt ≤ y.toInt
source
theorem Int16.le_iff_toInt_le {x y : Int16} :
x ≤ y ↔ x.toInt ≤ y.toInt
source
theorem Int32.le_iff_toInt_le {x y : Int32} :
x ≤ y ↔ x.toInt ≤ y.toInt
source
theorem Int64.le_iff_toInt_le {x y : Int64} :
x ≤ y ↔ x.toInt ≤ y.toInt
source
theorem ISize.le_iff_toInt_le {x y : ISize} :
x ≤ y ↔ x.toInt ≤ y.toInt
source
theorem Int8.lt_iff_toInt_lt {x y : Int8} :
x < y ↔ x.toInt < y.toInt
source
theorem Int16.lt_iff_toInt_lt {x y : Int16} :
x < y ↔ x.toInt < y.toInt
source
theorem Int32.lt_iff_toInt_lt {x y : Int32} :
x < y ↔ x.toInt < y.toInt
source
theorem Int64.lt_iff_toInt_lt {x y : Int64} :
x < y ↔ x.toInt < y.toInt
source
theorem ISize.lt_iff_toInt_lt {x y : ISize} :
x < y ↔ x.toInt < y.toInt
source
theorem Int8.cast_toNatClampNeg (x : Int8) (hx : 0 ≤ x) :
↑x.toNatClampNeg = x.toInt
source
theorem Int16.cast_toNatClampNeg (x : Int16) (hx : 0 ≤ x) :
↑x.toNatClampNeg = x.toInt
source
theorem Int32.cast_toNatClampNeg (x : Int32) (hx : 0 ≤ x) :
↑x.toNatClampNeg = x.toInt
source
theorem Int64.cast_toNatClampNeg (x : Int64) (hx : 0 ≤ x) :
↑x.toNatClampNeg = x.toInt
source
theorem ISize.cast_toNatClampNeg (x : ISize) (hx : 0 ≤ x) :
↑x.toNatClampNeg = x.toInt
source
theorem Int8.ofNat_toNatClampNeg (x : Int8) (hx : 0 ≤ x) :
ofNat x.toNatClampNeg = x
source
theorem Int16.ofNat_toNatClampNeg (x : Int16) (hx : 0 ≤ x) :
ofNat x.toNatClampNeg = x
source
theorem Int32.ofNat_toNatClampNeg (x : Int32) (hx : 0 ≤ x) :
ofNat x.toNatClampNeg = x
source
theorem Int64.ofNat_toNatClampNeg (x : Int64) (hx : 0 ≤ x) :
ofNat x.toNatClampNeg = x
source
theorem ISize.ofNat_toNatClampNeg (x : ISize) (hx : 0 ≤ x) :
ofNat x.toNatClampNeg = x
source
theorem Int16.ofNat_int8ToNatClampNeg (x : Int8) (hx : 0 ≤ x) :
ofNat x.toNatClampNeg = x.toInt16
source
theorem Int32.ofNat_int8ToNatClampNeg (x : Int8) (hx : 0 ≤ x) :
ofNat x.toNatClampNeg = x.toInt32
source
theorem Int64.ofNat_int8ToNatClampNeg (x : Int8) (hx : 0 ≤ x) :
ofNat x.toNatClampNeg = x.toInt64
source
theorem ISize.ofNat_int8ToNatClampNeg (x : Int8) (hx : 0 ≤ x) :
ofNat x.toNatClampNeg = x.toISize
source
theorem Int32.ofNat_int16ToNatClampNeg (x : Int16) (hx : 0 ≤ x) :
ofNat x.toNatClampNeg = x.toInt32
source
theorem Int64.ofNat_int16ToNatClampNeg (x : Int16) (hx : 0 ≤ x) :
ofNat x.toNatClampNeg = x.toInt64
source
theorem ISize.ofNat_int16ToNatClampNeg (x : Int16) (hx : 0 ≤ x) :
ofNat x.toNatClampNeg = x.toISize
source
theorem Int64.ofNat_int32ToNatClampNeg (x : Int32) (hx : 0 ≤ x) :
ofNat x.toNatClampNeg = x.toInt64
source
theorem ISize.ofNat_int32ToNatClampNeg (x : Int32) (hx : 0 ≤ x) :
ofNat x.toNatClampNeg = x.toISize
source
@[simp]
theorem Int8.toInt8_toInt16 (n : Int8) :
n.toInt16.toInt8 = n
source
@[simp]
theorem Int8.toInt8_toInt32 (n : Int8) :
n.toInt32.toInt8 = n
source
@[simp]
theorem Int8.toInt8_toInt64 (n : Int8) :
n.toInt64.toInt8 = n
source
@[simp]
theorem Int8.toInt8_toISize (n : Int8) :
n.toISize.toInt8 = n
source
@[simp]
theorem Int8.toInt16_toInt32 (n : Int8) :
n.toInt32.toInt16 = n.toInt16
source
@[simp]
theorem Int8.toInt16_toInt64 (n : Int8) :
n.toInt64.toInt16 = n.toInt16
source
@[simp]
theorem Int8.toInt16_toISize (n : Int8) :
n.toISize.toInt16 = n.toInt16
source
@[simp]
theorem Int8.toInt32_toInt16 (n : Int8) :
n.toInt16.toInt32 = n.toInt32
source
@[simp]
theorem Int8.toInt32_toInt64 (n : Int8) :
n.toInt64.toInt32 = n.toInt32
source
@[simp]
theorem Int8.toInt32_toISize (n : Int8) :
n.toISize.toInt32 = n.toInt32
source
@[simp]
theorem Int8.toInt64_toInt16 (n : Int8) :
n.toInt16.toInt64 = n.toInt64
source
@[simp]
theorem Int8.toInt64_toInt32 (n : Int8) :
n.toInt32.toInt64 = n.toInt64
source
@[simp]
theorem Int8.toInt64_toISize (n : Int8) :
n.toISize.toInt64 = n.toInt64
source
@[simp]
theorem Int8.toISize_toInt16 (n : Int8) :
n.toInt16.toISize = n.toISize
source
@[simp]
theorem Int8.toISize_toInt32 (n : Int8) :
n.toInt32.toISize = n.toISize
source
@[simp]
theorem Int8.toISize_toInt64 (n : Int8) :
n.toInt64.toISize = n.toISize
source
@[simp]
theorem Int16.toInt8_toInt32 (n : Int16) :
n.toInt32.toInt8 = n.toInt8
source
@[simp]
theorem Int16.toInt8_toInt64 (n : Int16) :
n.toInt64.toInt8 = n.toInt8
source
@[simp]
theorem Int16.toInt8_toISize (n : Int16) :
n.toISize.toInt8 = n.toInt8
source
@[simp]
theorem Int16.toInt16_toInt32 (n : Int16) :
n.toInt32.toInt16 = n
source
@[simp]
theorem Int16.toInt16_toInt64 (n : Int16) :
n.toInt64.toInt16 = n
source
@[simp]
theorem Int16.toInt16_toISize (n : Int16) :
n.toISize.toInt16 = n
source
@[simp]
theorem Int16.toInt32_toInt64 (n : Int16) :
n.toInt64.toInt32 = n.toInt32
source
@[simp]
theorem Int16.toInt32_toISize (n : Int16) :
n.toISize.toInt32 = n.toInt32
source
@[simp]
theorem Int16.toInt64_toInt32 (n : Int16) :
n.toInt32.toInt64 = n.toInt64
source
@[simp]
theorem Int16.toInt64_toISize (n : Int16) :
n.toISize.toInt64 = n.toInt64
source
@[simp]
theorem Int16.toISize_toInt32 (n : Int16) :
n.toInt32.toISize = n.toISize
source
@[simp]
theorem Int16.toISize_toInt64 (n : Int16) :
n.toInt64.toISize = n.toISize
source
@[simp]
theorem Int32.toInt8_toInt16 (n : Int32) :
n.toInt16.toInt8 = n.toInt8
source
@[simp]
theorem Int32.toInt8_toInt64 (n : Int32) :
n.toInt64.toInt8 = n.toInt8
source
@[simp]
theorem Int32.toInt8_toISize (n : Int32) :
n.toISize.toInt8 = n.toInt8
source
@[simp]
theorem Int32.toInt16_toInt64 (n : Int32) :
n.toInt64.toInt16 = n.toInt16
source
@[simp]
theorem Int32.toInt16_toISize (n : Int32) :
n.toISize.toInt16 = n.toInt16
source
@[simp]
theorem Int32.toInt32_toInt64 (n : Int32) :
n.toInt64.toInt32 = n
source
@[simp]
theorem Int32.toInt32_toISize (n : Int32) :
n.toISize.toInt32 = n
source
@[simp]
theorem Int32.toInt64_toISize (n : Int32) :
n.toISize.toInt64 = n.toInt64
source
@[simp]
theorem Int32.toISize_toInt64 (n : Int32) :
n.toInt64.toISize = n.toISize
source
@[simp]
theorem Int64.toInt8_toInt16 (n : Int64) :
n.toInt16.toInt8 = n.toInt8
source
@[simp]
theorem Int64.toInt8_toInt32 (n : Int64) :
n.toInt32.toInt8 = n.toInt8
source
@[simp]
theorem Int64.toInt8_toISize (n : Int64) :
n.toISize.toInt8 = n.toInt8
source
@[simp]
theorem Int64.toInt16_toInt32 (n : Int64) :
n.toInt32.toInt16 = n.toInt16
source
@[simp]
theorem Int64.toInt16_toISize (n : Int64) :
n.toISize.toInt16 = n.toInt16
source
@[simp]
theorem Int64.toInt32_toISize (n : Int64) :
n.toISize.toInt32 = n.toInt32
source
@[simp]
theorem ISize.toInt8_toInt16 (n : ISize) :
n.toInt16.toInt8 = n.toInt8
source
@[simp]
theorem ISize.toInt8_toInt32 (n : ISize) :
n.toInt32.toInt8 = n.toInt8
source
@[simp]
theorem ISize.toInt8_toInt64 (n : ISize) :
n.toInt64.toInt8 = n.toInt8
source
@[simp]
theorem ISize.toInt16_toInt32 (n : ISize) :
n.toInt32.toInt16 = n.toInt16
source
@[simp]
theorem ISize.toInt16_toInt64 (n : ISize) :
n.toInt64.toInt16 = n.toInt16
source
@[simp]
theorem ISize.toInt32_toInt64 (n : ISize) :
n.toInt64.toInt32 = n.toInt32
source
@[simp]
theorem ISize.toISize_toInt64 (n : ISize) :
n.toInt64.toISize = n
source
theorem UInt8.toInt8_ofNatLT {n : Nat} (hn : n < size) :
(ofNatLT n hn).toInt8 = Int8.ofNat n
source
theorem UInt16.toInt16_ofNatLT {n : Nat} (hn : n < size) :
(ofNatLT n hn).toInt16 = Int16.ofNat n
source
theorem UInt32.toInt32_ofNatLT {n : Nat} (hn : n < size) :
(ofNatLT n hn).toInt32 = Int32.ofNat n
source
theorem UInt64.toInt64_ofNatLT {n : Nat} (hn : n < size) :
(ofNatLT n hn).toInt64 = Int64.ofNat n
source
theorem USize.toISize_ofNatLT {n : Nat} (hn : n < size) :
(ofNatLT n hn).toISize = ISize.ofNat n
source
@[simp]
theorem UInt8.toInt8_ofNat' {n : Nat} :
(ofNat n).toInt8 = Int8.ofNat n
source
@[simp]
theorem UInt16.toInt16_ofNat' {n : Nat} :
(ofNat n).toInt16 = Int16.ofNat n
source
@[simp]
theorem UInt32.toInt32_ofNat' {n : Nat} :
(ofNat n).toInt32 = Int32.ofNat n
source
@[simp]
theorem UInt64.toInt64_ofNat' {n : Nat} :
(ofNat n).toInt64 = Int64.ofNat n
source
@[simp]
theorem USize.toISize_ofNat' {n : Nat} :
(ofNat n).toISize = ISize.ofNat n
source
@[simp]
theorem UInt8.toInt8_ofNat {n : Nat} :
(OfNat.ofNat n).toInt8 = OfNat.ofNat n
source
@[simp]
theorem UInt16.toInt16_ofNat {n : Nat} :
(OfNat.ofNat n).toInt16 = OfNat.ofNat n
source
@[simp]
theorem UInt32.toInt32_ofNat {n : Nat} :
(OfNat.ofNat n).toInt32 = OfNat.ofNat n
source
@[simp]
theorem UInt64.toInt64_ofNat {n : Nat} :
(OfNat.ofNat n).toInt64 = OfNat.ofNat n
source
@[simp]
theorem USize.toISize_ofNat {n : Nat} :
(OfNat.ofNat n).toISize = OfNat.ofNat n
source
@[simp]
theorem UInt8.toInt8_ofBitVec (b : BitVec 8) :
{ toBitVec := b }.toInt8 = Int8.ofBitVec b
source
@[simp]
theorem UInt16.toInt16_ofBitVec (b : BitVec 16) :
{ toBitVec := b }.toInt16 = Int16.ofBitVec b
source
@[simp]
theorem UInt32.toInt32_ofBitVec (b : BitVec 32) :
{ toBitVec := b }.toInt32 = Int32.ofBitVec b
source
@[simp]
theorem UInt64.toInt64_ofBitVec (b : BitVec 64) :
{ toBitVec := b }.toInt64 = Int64.ofBitVec b
source
@[simp]
theorem USize.toISize_ofBitVec (b : BitVec System.Platform.numBits) :
{ toBitVec := b }.toISize = ISize.ofBitVec b
source
@[simp]
theorem Int8.toBitVec_ofBitVec (b : BitVec 8) :
(ofBitVec b).toBitVec = b
source
@[simp]
theorem Int16.toBitVec_ofBitVec (b : BitVec 16) :
(ofBitVec b).toBitVec = b
source
@[simp]
theorem Int32.toBitVec_ofBitVec (b : BitVec 32) :
(ofBitVec b).toBitVec = b
source
@[simp]
theorem Int64.toBitVec_ofBitVec (b : BitVec 64) :
(ofBitVec b).toBitVec = b
source
@[simp]
theorem ISize.toBitVec_ofBitVec (b : BitVec System.Platform.numBits) :
(ofBitVec b).toBitVec = b
source
theorem Int8.toBitVec_ofIntTruncate {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) :
(ofIntTruncate n).toBitVec = BitVec.ofInt 8 n
source
theorem Int16.toBitVec_ofIntTruncate {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) :
(ofIntTruncate n).toBitVec = BitVec.ofInt 16 n
source
theorem Int32.toBitVec_ofIntTruncate {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) :
(ofIntTruncate n).toBitVec = BitVec.ofInt 32 n
source
theorem Int64.toBitVec_ofIntTruncate {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) :
(ofIntTruncate n).toBitVec = BitVec.ofInt 64 n
source
theorem ISize.toBitVec_ofIntTruncate {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) :
(ofIntTruncate n).toBitVec = BitVec.ofInt System.Platform.numBits n
source
@[simp]
theorem Int8.toInt_ofBitVec (b : BitVec 8) :
(ofBitVec b).toInt = b.toInt
source
@[simp]
theorem Int16.toInt_ofBitVec (b : BitVec 16) :
(ofBitVec b).toInt = b.toInt
source
@[simp]
theorem Int32.toInt_ofBitVec (b : BitVec 32) :
(ofBitVec b).toInt = b.toInt
source
@[simp]
theorem Int64.toInt_ofBitVec (b : BitVec 64) :
(ofBitVec b).toInt = b.toInt
source
@[simp]
theorem ISize.toInt_ofBitVec (b : BitVec System.Platform.numBits) :
(ofBitVec b).toInt = b.toInt
source
@[simp]
theorem Int8.toNatClampNeg_ofIntLE {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) :
(ofIntLE n h₁ h₂).toNatClampNeg = n.toNat
source
@[simp]
theorem Int16.toNatClampNeg_ofIntLE {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) :
(ofIntLE n h₁ h₂).toNatClampNeg = n.toNat
source
@[simp]
theorem Int32.toNatClampNeg_ofIntLE {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) :
(ofIntLE n h₁ h₂).toNatClampNeg = n.toNat
source
@[simp]
theorem Int64.toNatClampNeg_ofIntLE {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) :
(ofIntLE n h₁ h₂).toNatClampNeg = n.toNat
source
@[simp]
theorem ISize.toNatClampNeg_ofIntLE {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) :
(ofIntLE n h₁ h₂).toNatClampNeg = n.toNat
source
@[simp]
theorem Int8.toNatClampNeg_ofBitVec (b : BitVec 8) :
(ofBitVec b).toNatClampNeg = b.toInt.toNat
source
@[simp]
theorem Int16.toNatClampNeg_ofBitVec (b : BitVec 16) :
(ofBitVec b).toNatClampNeg = b.toInt.toNat
source
@[simp]
theorem Int32.toNatClampNeg_ofBitVec (b : BitVec 32) :
(ofBitVec b).toNatClampNeg = b.toInt.toNat
source
@[simp]
theorem Int64.toNatClampNeg_ofBitVec (b : BitVec 64) :
(ofBitVec b).toNatClampNeg = b.toInt.toNat
source
@[simp]
theorem ISize.toNatClampNeg_ofBitVec (b : BitVec System.Platform.numBits) :
(ofBitVec b).toNatClampNeg = b.toInt.toNat
source
theorem Int8.toNatClampNeg_ofInt_of_le {n : Int} (h₁ : -2 ^ 7 ≤ n) (h₂ : n < 2 ^ 7) :
(ofInt n).toNatClampNeg = n.toNat
source
theorem Int16.toNatClampNeg_ofInt_of_le {n : Int} (h₁ : -2 ^ 15 ≤ n) (h₂ : n < 2 ^ 15) :
(ofInt n).toNatClampNeg = n.toNat
source
theorem Int32.toNatClampNeg_ofInt_of_le {n : Int} (h₁ : -2 ^ 31 ≤ n) (h₂ : n < 2 ^ 31) :
(ofInt n).toNatClampNeg = n.toNat
source
theorem Int64.toNatClampNeg_ofInt_of_le {n : Int} (h₁ : -2 ^ 63 ≤ n) (h₂ : n < 2 ^ 63) :
(ofInt n).toNatClampNeg = n.toNat
source
theorem ISize.toNatClampNeg_ofInt_of_le {n : Int} (h₁ : -2 ^ 31 ≤ n) (h₂ : n < 2 ^ 31) :
(ofInt n).toNatClampNeg = n.toNat
source
theorem ISize.toNatClampNeg_ofInt_of_two_pow_numBits {n : Int} (h₁ : -2 ^ (System.Platform.numBits - 1) ≤ n) (h₂ : n < 2 ^ (System.Platform.numBits - 1)) :
(ofInt n).toNatClampNeg = n.toNat
source
theorem Int8.toNatClampNeg_ofIntTruncate_of_lt {n : Int} (h₁ : n < 2 ^ 7) :
(ofIntTruncate n).toNatClampNeg = n.toNat
source
theorem Int16.toNatClampNeg_ofIntTruncate_of_lt {n : Int} (h₁ : n < 2 ^ 15) :
(ofIntTruncate n).toNatClampNeg = n.toNat
source
theorem Int32.toNatClampNeg_ofIntTruncate_of_lt {n : Int} (h₁ : n < 2 ^ 31) :
(ofIntTruncate n).toNatClampNeg = n.toNat
source
theorem Int64.toNatClampNeg_ofIntTruncate_of_lt {n : Int} (h₁ : n < 2 ^ 63) :
(ofIntTruncate n).toNatClampNeg = n.toNat
source
theorem ISize.toNatClampNeg_ofIntTruncate_of_lt_two_pow_numBits {n : Int} (h₁ : n < 2 ^ (System.Platform.numBits - 1)) :
(ofIntTruncate n).toNatClampNeg = n.toNat
source
theorem ISize.toNatClampNeg_ofIntTruncate_of_lt {n : Int} (h₁ : n < 2 ^ 31) :
(ofIntTruncate n).toNatClampNeg = n.toNat
source
@[simp]
theorem Int8.toUInt8_ofBitVec (b : BitVec 8) :
(ofBitVec b).toUInt8 = { toBitVec := b }
source
@[simp]
theorem Int16.toUInt16_ofBitVec (b : BitVec 16) :
(ofBitVec b).toUInt16 = { toBitVec := b }
source
@[simp]
theorem Int32.toUInt32_ofBitVec (b : BitVec 32) :
(ofBitVec b).toUInt32 = { toBitVec := b }
source
@[simp]
theorem Int64.toUInt64_ofBitVec (b : BitVec 64) :
(ofBitVec b).toUInt64 = { toBitVec := b }
source
@[simp]
theorem ISize.toUSize_ofBitVec (b : BitVec System.Platform.numBits) :
(ofBitVec b).toUSize = { toBitVec := b }
source
@[simp]
theorem Int8.toUInt8_ofNat' {n : Nat} :
(ofNat n).toUInt8 = UInt8.ofNat n
source
@[simp]
theorem Int16.toUInt16_ofNat' {n : Nat} :
(ofNat n).toUInt16 = UInt16.ofNat n
source
@[simp]
theorem Int32.toUInt32_ofNat' {n : Nat} :
(ofNat n).toUInt32 = UInt32.ofNat n
source
@[simp]
theorem Int64.toUInt64_ofNat' {n : Nat} :
(ofNat n).toUInt64 = UInt64.ofNat n
source
@[simp]
theorem ISize.toUSize_ofNat' {n : Nat} :
(ofNat n).toUSize = USize.ofNat n
source
@[simp]
theorem Int8.toUInt8_ofNat {n : Nat} :
toUInt8 (OfNat.ofNat n) = OfNat.ofNat n
source
@[simp]
theorem Int16.toUInt16_ofNat {n : Nat} :
toUInt16 (OfNat.ofNat n) = OfNat.ofNat n
source
@[simp]
theorem Int32.toUInt32_ofNat {n : Nat} :
toUInt32 (OfNat.ofNat n) = OfNat.ofNat n
source
@[simp]
theorem Int64.toUInt64_ofNat {n : Nat} :
toUInt64 (OfNat.ofNat n) = OfNat.ofNat n
source
@[simp]
theorem ISize.toUSize_ofNat {n : Nat} :
toUSize (OfNat.ofNat n) = OfNat.ofNat n
source
theorem Int16.toInt8_ofIntLE {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) :
(ofIntLE n h₁ h₂).toInt8 = Int8.ofInt n
source
theorem Int32.toInt8_ofIntLE {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) :
(ofIntLE n h₁ h₂).toInt8 = Int8.ofInt n
source
theorem Int64.toInt8_ofIntLE {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) :
(ofIntLE n h₁ h₂).toInt8 = Int8.ofInt n
source
theorem ISize.toInt8_ofIntLE {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) :
(ofIntLE n h₁ h₂).toInt8 = Int8.ofInt n
source
@[simp]
theorem Int16.toInt8_ofBitVec (b : BitVec 16) :
(ofBitVec b).toInt8 = Int8.ofBitVec (BitVec.signExtend 8 b)
source
@[simp]
theorem Int32.toInt8_ofBitVec (b : BitVec 32) :
(ofBitVec b).toInt8 = Int8.ofBitVec (BitVec.signExtend 8 b)
source
@[simp]
theorem Int64.toInt8_ofBitVec (b : BitVec 64) :
(ofBitVec b).toInt8 = Int8.ofBitVec (BitVec.signExtend 8 b)
source
@[simp]
theorem ISize.toInt8_ofBitVec (b : BitVec System.Platform.numBits) :
(ofBitVec b).toInt8 = Int8.ofBitVec (BitVec.signExtend 8 b)
source
@[simp]
theorem Int16.toInt8_ofNat' {n : Nat} :
(ofNat n).toInt8 = Int8.ofNat n
source
@[simp]
theorem Int32.toInt8_ofNat' {n : Nat} :
(ofNat n).toInt8 = Int8.ofNat n
source
@[simp]
theorem Int64.toInt8_ofNat' {n : Nat} :
(ofNat n).toInt8 = Int8.ofNat n
source
@[simp]
theorem ISize.toInt8_ofNat' {n : Nat} :
(ofNat n).toInt8 = Int8.ofNat n
source
@[simp]
theorem Int16.toInt8_ofInt {n : Int} :
(ofInt n).toInt8 = Int8.ofInt n
source
@[simp]
theorem Int32.toInt8_ofInt {n : Int} :
(ofInt n).toInt8 = Int8.ofInt n
source
@[simp]
theorem Int64.toInt8_ofInt {n : Int} :
(ofInt n).toInt8 = Int8.ofInt n
source
@[simp]
theorem ISize.toInt8_ofInt {n : Int} :
(ofInt n).toInt8 = Int8.ofInt n
source
@[simp]
theorem Int16.toInt8_ofNat {n : Nat} :
(OfNat.ofNat n).toInt8 = OfNat.ofNat n
source
@[simp]
theorem Int32.toInt8_ofNat {n : Nat} :
(OfNat.ofNat n).toInt8 = OfNat.ofNat n
source
@[simp]
theorem Int64.toInt8_ofNat {n : Nat} :
(OfNat.ofNat n).toInt8 = OfNat.ofNat n
source
@[simp]
theorem ISize.toInt8_ofNat {n : Nat} :
(OfNat.ofNat n).toInt8 = OfNat.ofNat n
source
theorem Int16.toInt8_ofIntTruncate {n : Int} (h₁ : -2 ^ 15 ≤ n) (h₂ : n < 2 ^ 15) :
(ofIntTruncate n).toInt8 = Int8.ofInt n
source
theorem Int32.toInt8_ofIntTruncate {n : Int} (h₁ : -2 ^ 31 ≤ n) (h₂ : n < 2 ^ 31) :
(ofIntTruncate n).toInt8 = Int8.ofInt n
source
theorem Int64.toInt8_ofIntTruncate {n : Int} (h₁ : -2 ^ 63 ≤ n) (h₂ : n < 2 ^ 63) :
(ofIntTruncate n).toInt8 = Int8.ofInt n
source
theorem ISize.toInt8_ofIntTruncate {n : Int} (h₁ : -2 ^ (System.Platform.numBits - 1) ≤ n) (h₂ : n < 2 ^ (System.Platform.numBits - 1)) :
(ofIntTruncate n).toInt8 = Int8.ofInt n
source
theorem Int32.toInt16_ofIntLE {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) :
(ofIntLE n h₁ h₂).toInt16 = Int16.ofInt n
source
theorem Int64.toInt16_ofIntLE {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) :
(ofIntLE n h₁ h₂).toInt16 = Int16.ofInt n
source
theorem ISize.toInt16_ofIntLE {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) :
(ofIntLE n h₁ h₂).toInt16 = Int16.ofInt n
source
@[simp]
theorem Int32.toInt16_ofBitVec (b : BitVec 32) :
(ofBitVec b).toInt16 = Int16.ofBitVec (BitVec.signExtend 16 b)
source
@[simp]
theorem Int64.toInt16_ofBitVec (b : BitVec 64) :
(ofBitVec b).toInt16 = Int16.ofBitVec (BitVec.signExtend 16 b)
source
@[simp]
theorem ISize.toInt16_ofBitVec (b : BitVec System.Platform.numBits) :
(ofBitVec b).toInt16 = Int16.ofBitVec (BitVec.signExtend 16 b)
source
@[simp]
theorem Int32.toInt16_ofNat' {n : Nat} :
(ofNat n).toInt16 = Int16.ofNat n
source
@[simp]
theorem Int64.toInt16_ofNat' {n : Nat} :
(ofNat n).toInt16 = Int16.ofNat n
source
@[simp]
theorem ISize.toInt16_ofNat' {n : Nat} :
(ofNat n).toInt16 = Int16.ofNat n
source
@[simp]
theorem Int32.toInt16_ofInt {n : Int} :
(ofInt n).toInt16 = Int16.ofInt n
source
@[simp]
theorem Int64.toInt16_ofInt {n : Int} :
(ofInt n).toInt16 = Int16.ofInt n
source
@[simp]
theorem ISize.toInt16_ofInt {n : Int} :
(ofInt n).toInt16 = Int16.ofInt n
source
@[simp]
theorem Int32.toInt16_ofNat {n : Nat} :
(OfNat.ofNat n).toInt16 = OfNat.ofNat n
source
@[simp]
theorem Int64.toInt16_ofNat {n : Nat} :
(OfNat.ofNat n).toInt16 = OfNat.ofNat n
source
@[simp]
theorem ISize.toInt16_ofNat {n : Nat} :
(OfNat.ofNat n).toInt16 = OfNat.ofNat n
source
theorem Int32.toInt16_ofIntTruncate {n : Int} (h₁ : -2 ^ 31 ≤ n) (h₂ : n < 2 ^ 31) :
(ofIntTruncate n).toInt16 = Int16.ofInt n
source
theorem Int64.toInt16_ofIntTruncate {n : Int} (h₁ : -2 ^ 63 ≤ n) (h₂ : n < 2 ^ 63) :
(ofIntTruncate n).toInt16 = Int16.ofInt n
source
theorem ISize.toInt16_ofIntTruncate {n : Int} (h₁ : -2 ^ (System.Platform.numBits - 1) ≤ n) (h₂ : n < 2 ^ (System.Platform.numBits - 1)) :
(ofIntTruncate n).toInt16 = Int16.ofInt n
source
theorem Int64.toInt32_ofIntLE {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) :
(ofIntLE n h₁ h₂).toInt32 = Int32.ofInt n
source
theorem ISize.toInt32_ofIntLE {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) :
(ofIntLE n h₁ h₂).toInt32 = Int32.ofInt n
source
@[simp]
theorem Int64.toInt32_ofBitVec (b : BitVec 64) :
(ofBitVec b).toInt32 = Int32.ofBitVec (BitVec.signExtend 32 b)
source
@[simp]
theorem ISize.toInt32_ofBitVec (b : BitVec System.Platform.numBits) :
(ofBitVec b).toInt32 = Int32.ofBitVec (BitVec.signExtend 32 b)
source
@[simp]
theorem Int64.toInt32_ofNat' {n : Nat} :
(ofNat n).toInt32 = Int32.ofNat n
source
@[simp]
theorem ISize.toInt32_ofNat' {n : Nat} :
(ofNat n).toInt32 = Int32.ofNat n
source
@[simp]
theorem Int64.toInt32_ofInt {n : Int} :
(ofInt n).toInt32 = Int32.ofInt n
source
@[simp]
theorem ISize.toInt32_ofInt {n : Int} :
(ofInt n).toInt32 = Int32.ofInt n
source
@[simp]
theorem Int64.toInt32_ofNat {n : Nat} :
(OfNat.ofNat n).toInt32 = OfNat.ofNat n
source
@[simp]
theorem ISize.toInt32_ofNat {n : Nat} :
(OfNat.ofNat n).toInt32 = OfNat.ofNat n
source
theorem Int64.toInt32_ofIntTruncate {n : Int} (h₁ : -2 ^ 63 ≤ n) (h₂ : n < 2 ^ 63) :
(ofIntTruncate n).toInt32 = Int32.ofInt n
source
theorem ISize.toInt32_ofIntTruncate {n : Int} (h₁ : -2 ^ (System.Platform.numBits - 1) ≤ n) (h₂ : n < 2 ^ (System.Platform.numBits - 1)) :
(ofIntTruncate n).toInt32 = Int32.ofInt n
source
theorem Int64.toISize_ofIntLE {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) :
(ofIntLE n h₁ h₂).toISize = ISize.ofInt n
source
@[simp]
theorem Int64.toISize_ofBitVec (b : BitVec 64) :
(ofBitVec b).toISize = ISize.ofBitVec (BitVec.signExtend System.Platform.numBits b)
source
@[simp]
theorem Int64.toISize_ofNat' {n : Nat} :
(ofNat n).toISize = ISize.ofNat n
source
@[simp]
theorem Int64.toISize_ofInt {n : Int} :
(ofInt n).toISize = ISize.ofInt n
source
@[simp]
theorem Int64.toISize_ofNat {n : Nat} :
(OfNat.ofNat n).toISize = OfNat.ofNat n
source
theorem Int64.toISize_ofIntTruncate {n : Int} (h₁ : -2 ^ 63 ≤ n) (h₂ : n < 2 ^ 63) :
(ofIntTruncate n).toISize = ISize.ofInt n
source
@[simp]
theorem Int8.toBitVec_minValue :
minValue.toBitVec = BitVec.intMin 8
source
@[simp]
theorem Int16.toBitVec_minValue :
minValue.toBitVec = BitVec.intMin 16
source
@[simp]
theorem Int32.toBitVec_minValue :
minValue.toBitVec = BitVec.intMin 32
source
@[simp]
theorem Int64.toBitVec_minValue :
minValue.toBitVec = BitVec.intMin 64
source
@[simp]
theorem ISize.toBitVec_minValue :
minValue.toBitVec = BitVec.intMin System.Platform.numBits
source
@[simp]
theorem Int8.toBitVec_maxValue :
maxValue.toBitVec = BitVec.intMax 8
source
@[simp]
theorem Int16.toBitVec_maxValue :
maxValue.toBitVec = BitVec.intMax 16
source
@[simp]
theorem Int32.toBitVec_maxValue :
maxValue.toBitVec = BitVec.intMax 32
source
@[simp]
theorem Int64.toBitVec_maxValue :
maxValue.toBitVec = BitVec.intMax 64
source
@[simp]
theorem ISize.toBitVec_maxValue :
maxValue.toBitVec = BitVec.intMax System.Platform.numBits
source
@[simp]
theorem Int16.toInt8_neg (x : Int16) :
(-x).toInt8 = -x.toInt8
source
@[simp]
theorem Int32.toInt8_neg (x : Int32) :
(-x).toInt8 = -x.toInt8
source
@[simp]
theorem Int64.toInt8_neg (x : Int64) :
(-x).toInt8 = -x.toInt8
source
@[simp]
theorem ISize.toInt8_neg (x : ISize) :
(-x).toInt8 = -x.toInt8
source
@[simp]
theorem Int32.toInt16_neg (x : Int32) :
(-x).toInt16 = -x.toInt16
source
@[simp]
theorem Int64.toInt16_neg (x : Int64) :
(-x).toInt16 = -x.toInt16
source
@[simp]
theorem ISize.toInt16_neg (x : ISize) :
(-x).toInt16 = -x.toInt16
source
@[simp]
theorem Int64.toInt32_neg (x : Int64) :
(-x).toInt32 = -x.toInt32
source
@[simp]
theorem ISize.toInt32_neg (x : ISize) :
(-x).toInt32 = -x.toInt32
source
@[simp]
theorem Int64.toISize_neg (x : Int64) :
(-x).toISize = -x.toISize
source
@[simp]
theorem Int8.toInt16_neg_of_ne {x : Int8} (hx : x ≠ -128) :
(-x).toInt16 = -x.toInt16
source
@[simp]
theorem Int8.toInt32_neg_of_ne {x : Int8} (hx : x ≠ -128) :
(-x).toInt32 = -x.toInt32
source
@[simp]
theorem Int16.toInt32_neg_of_ne {x : Int16} (hx : x ≠ -32768) :
(-x).toInt32 = -x.toInt32
source
@[simp]
theorem Int8.toISize_neg_of_ne {x : Int8} (hx : x ≠ -128) :
(-x).toISize = -x.toISize
source
@[simp]
theorem Int16.toISize_neg_of_ne {x : Int16} (hx : x ≠ -32768) :
(-x).toISize = -x.toISize
source
@[simp]
theorem Int32.toISize_neg_of_ne {x : Int32} (hx : x ≠ -2147483648) :
(-x).toISize = -x.toISize
source
@[simp]
theorem Int8.toInt64_neg_of_ne {x : Int8} (hx : x ≠ -128) :
(-x).toInt64 = -x.toInt64
source
@[simp]
theorem Int16.toInt64_neg_of_ne {x : Int16} (hx : x ≠ -32768) :
(-x).toInt64 = -x.toInt64
source
@[simp]
theorem Int32.toInt64_neg_of_ne {x : Int32} (hx : x ≠ -2147483648) :
(-x).toInt64 = -x.toInt64
source
@[simp]
theorem ISize.toInt64_neg_of_ne {x : ISize} (hx : x ≠ minValue) :
(-x).toInt64 = -x.toInt64
source
theorem Int8.toInt16_ofIntLE {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) :
(ofIntLE n h₁ h₂).toInt16 = Int16.ofIntLE n ⋯ ⋯
source
theorem Int8.toInt32_ofIntLE {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) :
(ofIntLE n h₁ h₂).toInt32 = Int32.ofIntLE n ⋯ ⋯
source
theorem Int8.toInt64_ofIntLE {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) :
(ofIntLE n h₁ h₂).toInt64 = Int64.ofIntLE n ⋯ ⋯
source
theorem Int8.toISize_ofIntLE {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) :
(ofIntLE n h₁ h₂).toISize = ISize.ofIntLE n ⋯ ⋯
source
@[simp]
theorem Int8.toInt16_ofBitVec (b : BitVec 8) :
(ofBitVec b).toInt16 = Int16.ofBitVec (BitVec.signExtend 16 b)
source
@[simp]
theorem Int8.toInt32_ofBitVec (b : BitVec 8) :
(ofBitVec b).toInt32 = Int32.ofBitVec (BitVec.signExtend 32 b)
source
@[simp]
theorem Int8.toInt64_ofBitVec (b : BitVec 8) :
(ofBitVec b).toInt64 = Int64.ofBitVec (BitVec.signExtend 64 b)
source
@[simp]
theorem Int8.toISize_ofBitVec (b : BitVec 8) :
(ofBitVec b).toISize = ISize.ofBitVec (BitVec.signExtend System.Platform.numBits b)
source
@[simp]
theorem Int8.toInt16_ofInt {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) :
(ofInt n).toInt16 = Int16.ofInt n
source
@[simp]
theorem Int8.toInt32_ofInt {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) :
(ofInt n).toInt32 = Int32.ofInt n
source
@[simp]
theorem Int8.toInt64_ofInt {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) :
(ofInt n).toInt64 = Int64.ofInt n
source
@[simp]
theorem Int8.toISize_ofInt {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) :
(ofInt n).toISize = ISize.ofInt n
source
@[simp]
theorem Int8.toInt16_ofNat' {n : Nat} (h : ↑n ≤ maxValue.toInt) :
(ofNat n).toInt16 = Int16.ofNat n
source
@[simp]
theorem Int8.toInt32_ofNat' {n : Nat} (h : ↑n ≤ maxValue.toInt) :
(ofNat n).toInt32 = Int32.ofNat n
source
@[simp]
theorem Int8.toInt64_ofNat' {n : Nat} (h : ↑n ≤ maxValue.toInt) :
(ofNat n).toInt64 = Int64.ofNat n
source
@[simp]
theorem Int8.toISize_ofNat' {n : Nat} (h : ↑n ≤ maxValue.toInt) :
(ofNat n).toISize = ISize.ofNat n
source
@[simp]
theorem Int8.toInt16_ofNat {n : Nat} (h : n ≤ 127) :
(OfNat.ofNat n).toInt16 = OfNat.ofNat n
source
@[simp]
theorem Int8.toInt32_ofNat {n : Nat} (h : n ≤ 127) :
(OfNat.ofNat n).toInt32 = OfNat.ofNat n
source
@[simp]
theorem Int8.toInt64_ofNat {n : Nat} (h : n ≤ 127) :
(OfNat.ofNat n).toInt64 = OfNat.ofNat n
source
@[simp]
theorem Int8.toISize_ofNat {n : Nat} (h : n ≤ 127) :
(OfNat.ofNat n).toISize = OfNat.ofNat n
source
theorem Int16.toInt32_ofIntLE {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) :
(ofIntLE n h₁ h₂).toInt32 = Int32.ofIntLE n ⋯ ⋯
source
theorem Int16.toInt64_ofIntLE {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) :
(ofIntLE n h₁ h₂).toInt64 = Int64.ofIntLE n ⋯ ⋯
source
theorem Int16.toISize_ofIntLE {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) :
(ofIntLE n h₁ h₂).toISize = ISize.ofIntLE n ⋯ ⋯
source
@[simp]
theorem Int16.toInt32_ofBitVec (b : BitVec 16) :
(ofBitVec b).toInt32 = Int32.ofBitVec (BitVec.signExtend 32 b)
source
@[simp]
theorem Int16.toInt64_ofBitVec (b : BitVec 16) :
(ofBitVec b).toInt64 = Int64.ofBitVec (BitVec.signExtend 64 b)
source
@[simp]
theorem Int16.toISize_ofBitVec (b : BitVec 16) :
(ofBitVec b).toISize = ISize.ofBitVec (BitVec.signExtend System.Platform.numBits b)
source
@[simp]
theorem Int16.toInt32_ofInt {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) :
(ofInt n).toInt32 = Int32.ofInt n
source
@[simp]
theorem Int16.toInt64_ofInt {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) :
(ofInt n).toInt64 = Int64.ofInt n
source
@[simp]
theorem Int16.toISize_ofInt {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) :
(ofInt n).toISize = ISize.ofInt n
source
@[simp]
theorem Int16.toInt32_ofNat' {n : Nat} (h : ↑n ≤ maxValue.toInt) :
(ofNat n).toInt32 = Int32.ofNat n
source
@[simp]
theorem Int16.toInt64_ofNat' {n : Nat} (h : ↑n ≤ maxValue.toInt) :
(ofNat n).toInt64 = Int64.ofNat n
source
@[simp]
theorem Int16.toISize_ofNat' {n : Nat} (h : ↑n ≤ maxValue.toInt) :
(ofNat n).toISize = ISize.ofNat n
source
@[simp]
theorem Int16.toInt32_ofNat {n : Nat} (h : n ≤ 32767) :
(OfNat.ofNat n).toInt32 = OfNat.ofNat n
source
@[simp]
theorem Int16.toInt64_ofNat {n : Nat} (h : n ≤ 32767) :
(OfNat.ofNat n).toInt64 = OfNat.ofNat n
source
@[simp]
theorem Int16.toISize_ofNat {n : Nat} (h : n ≤ 32767) :
(OfNat.ofNat n).toISize = OfNat.ofNat n
source
theorem Int32.toInt64_ofIntLE {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) :
(ofIntLE n h₁ h₂).toInt64 = Int64.ofIntLE n ⋯ ⋯
source
theorem Int32.toISize_ofIntLE {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) :
(ofIntLE n h₁ h₂).toISize = ISize.ofIntLE n ⋯ ⋯
source
@[simp]
theorem Int32.toInt64_ofBitVec (b : BitVec 32) :
(ofBitVec b).toInt64 = Int64.ofBitVec (BitVec.signExtend 64 b)
source
@[simp]
theorem Int32.toISize_ofBitVec (b : BitVec 32) :
(ofBitVec b).toISize = ISize.ofBitVec (BitVec.signExtend System.Platform.numBits b)
source
@[simp]
theorem Int32.toInt64_ofInt {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) :
(ofInt n).toInt64 = Int64.ofInt n
source
@[simp]
theorem Int32.toISize_ofInt {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) :
(ofInt n).toISize = ISize.ofInt n
source
@[simp]
theorem Int32.toInt64_ofNat' {n : Nat} (h : ↑n ≤ maxValue.toInt) :
(ofNat n).toInt64 = Int64.ofNat n
source
@[simp]
theorem Int32.toISize_ofNat' {n : Nat} (h : ↑n ≤ maxValue.toInt) :
(ofNat n).toISize = ISize.ofNat n
source
@[simp]
theorem Int32.toInt64_ofNat {n : Nat} (h : n ≤ 2147483647) :
(OfNat.ofNat n).toInt64 = OfNat.ofNat n
source
@[simp]
theorem Int32.toISize_ofNat {n : Nat} (h : n ≤ 2147483647) :
(OfNat.ofNat n).toISize = OfNat.ofNat n
source
theorem ISize.toInt64_ofIntLE {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) :
(ofIntLE n h₁ h₂).toInt64 = Int64.ofIntLE n ⋯ ⋯
source
@[simp]
theorem ISize.toInt64_ofBitVec (b : BitVec System.Platform.numBits) :
(ofBitVec b).toInt64 = Int64.ofBitVec (BitVec.signExtend 64 b)
source
@[simp]
theorem ISize.toInt64_ofInt {n : Int} (h₁ : minValue.toInt ≤ n) (h₂ : n ≤ maxValue.toInt) :
(ofInt n).toInt64 = Int64.ofInt n
source
@[simp]
theorem ISize.toInt64_ofNat' {n : Nat} (h : ↑n ≤ maxValue.toInt) :
(ofNat n).toInt64 = Int64.ofNat n
source
@[simp]
theorem ISize.toInt64_ofNat {n : Nat} (h : n ≤ 2147483647) :
(OfNat.ofNat n).toInt64 = OfNat.ofNat n
source
@[simp]
theorem Int8.ofIntLE_bitVecToInt (n : BitVec 8) :
ofIntLE n.toInt ⋯ ⋯ = ofBitVec n
source
@[simp]
theorem Int16.ofIntLE_bitVecToInt (n : BitVec 16) :
ofIntLE n.toInt ⋯ ⋯ = ofBitVec n
source
@[simp]
theorem Int32.ofIntLE_bitVecToInt (n : BitVec 32) :
ofIntLE n.toInt ⋯ ⋯ = ofBitVec n
source
@[simp]
theorem Int64.ofIntLE_bitVecToInt (n : BitVec 64) :
ofIntLE n.toInt ⋯ ⋯ = ofBitVec n
source
@[simp]
theorem ISize.ofIntLE_bitVecToInt (n : BitVec System.Platform.numBits) :
ofIntLE n.toInt ⋯ ⋯ = ofBitVec n
source
theorem Int8.ofBitVec_ofNatLT (n : Nat) (hn : n < 2 ^ 8) :
ofBitVec n#'hn = ofNat n
source
theorem Int16.ofBitVec_ofNatLT (n : Nat) (hn : n < 2 ^ 16) :
ofBitVec n#'hn = ofNat n
source
theorem Int32.ofBitVec_ofNatLT (n : Nat) (hn : n < 2 ^ 32) :
ofBitVec n#'hn = ofNat n
source
theorem Int64.ofBitVec_ofNatLT (n : Nat) (hn : n < 2 ^ 64) :
ofBitVec n#'hn = ofNat n
source
theorem ISize.ofBitVec_ofNatLT (n : Nat) (hn : n < 2 ^ System.Platform.numBits) :
ofBitVec n#'hn = ofNat n
source
@[simp]
theorem Int8.ofBitVec_ofNat (n : Nat) :
ofBitVec (BitVec.ofNat 8 n) = ofNat n
source
@[simp]
theorem Int16.ofBitVec_ofNat (n : Nat) :
ofBitVec (BitVec.ofNat 16 n) = ofNat n
source
@[simp]
theorem Int32.ofBitVec_ofNat (n : Nat) :
ofBitVec (BitVec.ofNat 32 n) = ofNat n
source
@[simp]
theorem Int64.ofBitVec_ofNat (n : Nat) :
ofBitVec (BitVec.ofNat 64 n) = ofNat n
source
@[simp]
theorem ISize.ofBitVec_ofNat (n : Nat) :
ofBitVec (BitVec.ofNat System.Platform.numBits n) = ofNat n
source
@[simp]
theorem Int8.ofBitVec_ofInt (n : Int) :
ofBitVec (BitVec.ofInt 8 n) = ofInt n
source
@[simp]
theorem Int16.ofBitVec_ofInt (n : Int) :
ofBitVec (BitVec.ofInt 16 n) = ofInt n
source
@[simp]
theorem Int32.ofBitVec_ofInt (n : Int) :
ofBitVec (BitVec.ofInt 32 n) = ofInt n
source
@[simp]
theorem Int64.ofBitVec_ofInt (n : Int) :
ofBitVec (BitVec.ofInt 64 n) = ofInt n
source
@[simp]
theorem ISize.ofBitVec_ofInt (n : Int) :
ofBitVec (BitVec.ofInt System.Platform.numBits n) = ofInt n
source
@[simp]
theorem Int8.ofNat_bitVecToNat (n : BitVec 8) :
ofNat n.toNat = ofBitVec n
source
@[simp]
theorem Int16.ofNat_bitVecToNat (n : BitVec 16) :
ofNat n.toNat = ofBitVec n
source
@[simp]
theorem Int32.ofNat_bitVecToNat (n : BitVec 32) :
ofNat n.toNat = ofBitVec n
source
@[simp]
theorem Int64.ofNat_bitVecToNat (n : BitVec 64) :
ofNat n.toNat = ofBitVec n
source
@[simp]
theorem ISize.ofNat_bitVecToNat (n : BitVec System.Platform.numBits) :
ofNat n.toNat = ofBitVec n
source
@[simp]
theorem Int8.ofInt_bitVecToInt (n : BitVec 8) :
ofInt n.toInt = ofBitVec n
source
@[simp]
theorem Int16.ofInt_bitVecToInt (n : BitVec 16) :
ofInt n.toInt = ofBitVec n
source
@[simp]
theorem Int32.ofInt_bitVecToInt (n : BitVec 32) :
ofInt n.toInt = ofBitVec n
source
@[simp]
theorem Int64.ofInt_bitVecToInt (n : BitVec 64) :
ofInt n.toInt = ofBitVec n
source
@[simp]
theorem ISize.ofInt_bitVecToInt (n : BitVec System.Platform.numBits) :
ofInt n.toInt = ofBitVec n
source
@[simp]
theorem Int8.ofIntTruncate_bitVecToInt (n : BitVec 8) :
ofIntTruncate n.toInt = ofBitVec n
source
@[simp]
theorem Int16.ofIntTruncate_bitVecToInt (n : BitVec 16) :
ofIntTruncate n.toInt = ofBitVec n
source
@[simp]
theorem Int32.ofIntTruncate_bitVecToInt (n : BitVec 32) :
ofIntTruncate n.toInt = ofBitVec n
source
@[simp]
theorem Int64.ofIntTruncate_bitVecToInt (n : BitVec 64) :
ofIntTruncate n.toInt = ofBitVec n
source
@[simp]
theorem ISize.ofIntTruncate_bitVecToInt (n : BitVec System.Platform.numBits) :
ofIntTruncate n.toInt = ofBitVec n
source
@[simp]
theorem Int8.toInt_neg (n : Int8) :
(-n).toInt = (-n.toInt).bmod (2 ^ 8)
source
@[simp]
theorem Int16.toInt_neg (n : Int16) :
(-n).toInt = (-n.toInt).bmod (2 ^ 16)
source
@[simp]
theorem Int32.toInt_neg (n : Int32) :
(-n).toInt = (-n.toInt).bmod (2 ^ 32)
source
@[simp]
theorem Int64.toInt_neg (n : Int64) :
(-n).toInt = (-n.toInt).bmod (2 ^ 64)
source
theorem ISize.toInt_neg (n : ISize) :
(-n).toInt = (-n.toInt).bmod (2 ^ System.Platform.numBits)
source
@[simp]
theorem Int8.toNatClampNeg_eq_zero_iff {n : Int8} :
n.toNatClampNeg = 0 ↔ n ≤ 0
source
@[simp]
theorem Int16.toNatClampNeg_eq_zero_iff {n : Int16} :
n.toNatClampNeg = 0 ↔ n ≤ 0
source
@[simp]
theorem Int32.toNatClampNeg_eq_zero_iff {n : Int32} :
n.toNatClampNeg = 0 ↔ n ≤ 0
source
@[simp]
theorem Int64.toNatClampNeg_eq_zero_iff {n : Int64} :
n.toNatClampNeg = 0 ↔ n ≤ 0
source
@[simp]
theorem ISize.toNatClampNeg_eq_zero_iff {n : ISize} :
n.toNatClampNeg = 0 ↔ n ≤ 0
source
@[simp]
theorem Int8.not_le {n m : Int8} :
¬n ≤ m ↔ m < n
source
@[simp]
theorem Int16.not_le {n m : Int16} :
¬n ≤ m ↔ m < n
source
@[simp]
theorem Int32.not_le {n m : Int32} :
¬n ≤ m ↔ m < n
source
@[simp]
theorem Int64.not_le {n m : Int64} :
¬n ≤ m ↔ m < n
source
@[simp]
theorem ISize.not_le {n m : ISize} :
¬n ≤ m ↔ m < n
source
@[simp]
theorem Int8.neg_nonpos_iff (n : Int8) :
-n ≤ 0 ↔ n = minValue ∨ 0 ≤ n
source
@[simp]
theorem Int16.neg_nonpos_iff (n : Int16) :
-n ≤ 0 ↔ n = minValue ∨ 0 ≤ n
source
@[simp]
theorem Int32.neg_nonpos_iff (n : Int32) :
-n ≤ 0 ↔ n = minValue ∨ 0 ≤ n
source
@[simp]
theorem Int64.neg_nonpos_iff (n : Int64) :
-n ≤ 0 ↔ n = minValue ∨ 0 ≤ n
source
@[simp]
theorem ISize.neg_nonpos_iff (n : ISize) :
-n ≤ 0 ↔ n = minValue ∨ 0 ≤ n
source
@[simp]
theorem Int8.toNatClampNeg_pos_iff (n : Int8) :
0 < n.toNatClampNeg ↔ 0 < n
source
@[simp]
theorem Int16.toNatClampNeg_pos_iff (n : Int16) :
0 < n.toNatClampNeg ↔ 0 < n
source
@[simp]
theorem Int32.toNatClampNeg_pos_iff (n : Int32) :
0 < n.toNatClampNeg ↔ 0 < n
source
@[simp]
theorem Int64.toNatClampNeg_pos_iff (n : Int64) :
0 < n.toNatClampNeg ↔ 0 < n
source
@[simp]
theorem ISize.toNatClampNeg_pos_iff (n : ISize) :
0 < n.toNatClampNeg ↔ 0 < n
source
@[simp]
theorem Int8.toInt_div (a b : Int8) :
(a / b).toInt = (a.toInt.tdiv b.toInt).bmod (2 ^ 8)
source
@[simp]
theorem Int16.toInt_div (a b : Int16) :
(a / b).toInt = (a.toInt.tdiv b.toInt).bmod (2 ^ 16)
source
@[simp]
theorem Int32.toInt_div (a b : Int32) :
(a / b).toInt = (a.toInt.tdiv b.toInt).bmod (2 ^ 32)
source
@[simp]
theorem Int64.toInt_div (a b : Int64) :
(a / b).toInt = (a.toInt.tdiv b.toInt).bmod (2 ^ 64)
source
@[simp]
theorem ISize.toInt_div (a b : ISize) :
(a / b).toInt = (a.toInt.tdiv b.toInt).bmod (2 ^ System.Platform.numBits)
source
theorem Int8.toInt_div_of_ne_left (a b : Int8) (h : a ≠ minValue) :
(a / b).toInt = a.toInt.tdiv b.toInt
source
theorem Int16.toInt_div_of_ne_left (a b : Int16) (h : a ≠ minValue) :
(a / b).toInt = a.toInt.tdiv b.toInt
source
theorem Int32.toInt_div_of_ne_left (a b : Int32) (h : a ≠ minValue) :
(a / b).toInt = a.toInt.tdiv b.toInt
source
theorem Int64.toInt_div_of_ne_left (a b : Int64) (h : a ≠ minValue) :
(a / b).toInt = a.toInt.tdiv b.toInt
source
theorem ISize.toInt_div_of_ne_left (a b : ISize) (h : a ≠ minValue) :
(a / b).toInt = a.toInt.tdiv b.toInt
source
theorem Int8.toInt_div_of_ne_right (a b : Int8) (h : b ≠ -1) :
(a / b).toInt = a.toInt.tdiv b.toInt
source
theorem Int16.toInt_div_of_ne_right (a b : Int16) (h : b ≠ -1) :
(a / b).toInt = a.toInt.tdiv b.toInt
source
theorem Int32.toInt_div_of_ne_right (a b : Int32) (h : b ≠ -1) :
(a / b).toInt = a.toInt.tdiv b.toInt
source
theorem Int64.toInt_div_of_ne_right (a b : Int64) (h : b ≠ -1) :
(a / b).toInt = a.toInt.tdiv b.toInt
source
theorem ISize.toInt_div_of_ne_right (a b : ISize) (h : b ≠ -1) :
(a / b).toInt = a.toInt.tdiv b.toInt
source
theorem Int8.toInt16_ne_minValue (a : Int8) :
a.toInt16 ≠ Int16.minValue
source
theorem Int8.toInt32_ne_minValue (a : Int8) :
a.toInt32 ≠ Int32.minValue
source
theorem Int8.toInt64_ne_minValue (a : Int8) :
a.toInt64 ≠ Int64.minValue
source
theorem Int8.toISize_ne_minValue (a : Int8) :
a.toISize ≠ ISize.minValue
source
theorem Int16.toInt32_ne_minValue (a : Int16) :
a.toInt32 ≠ Int32.minValue
source
theorem Int16.toInt64_ne_minValue (a : Int16) :
a.toInt64 ≠ Int64.minValue
source
theorem Int16.toISize_ne_minValue (a : Int16) :
a.toISize ≠ ISize.minValue
source
theorem Int32.toInt64_ne_minValue (a : Int32) :
a.toInt64 ≠ Int64.minValue
source
theorem Int32.toISize_ne_minValue (a : Int32) (ha : a ≠ minValue) :
a.toISize ≠ ISize.minValue
source
theorem ISize.toInt64_ne_minValue (a : ISize) (ha : a ≠ minValue) :
a.toInt64 ≠ Int64.minValue
source
theorem Int8.toInt16_ne_neg_one (a : Int8) (ha : a ≠ -1) :
a.toInt16 ≠ -1
source
theorem Int8.toInt32_ne_neg_one (a : Int8) (ha : a ≠ -1) :
a.toInt32 ≠ -1
source
theorem Int8.toInt64_ne_neg_one (a : Int8) (ha : a ≠ -1) :
a.toInt64 ≠ -1
source
theorem Int8.toISize_ne_neg_one (a : Int8) (ha : a ≠ -1) :
a.toISize ≠ -1
source
theorem Int16.toInt32_ne_neg_one (a : Int16) (ha : a ≠ -1) :
a.toInt32 ≠ -1
source
theorem Int16.toInt64_ne_neg_one (a : Int16) (ha : a ≠ -1) :
a.toInt64 ≠ -1
source
theorem Int16.toISize_ne_neg_one (a : Int16) (ha : a ≠ -1) :
a.toISize ≠ -1
source
theorem Int32.toInt64_ne_neg_one (a : Int32) (ha : a ≠ -1) :
a.toInt64 ≠ -1
source
theorem Int32.toISize_ne_neg_one (a : Int32) (ha : a ≠ -1) :
a.toISize ≠ -1
source
theorem ISize.toInt64_ne_neg_one (a : ISize) (ha : a ≠ -1) :
a.toInt64 ≠ -1
source
theorem Int8.toInt16_div_of_ne_left (a b : Int8) (ha : a ≠ minValue) :
(a / b).toInt16 = a.toInt16 / b.toInt16
source
theorem Int8.toInt32_div_of_ne_left (a b : Int8) (ha : a ≠ minValue) :
(a / b).toInt32 = a.toInt32 / b.toInt32
source
theorem Int8.toInt64_div_of_ne_left (a b : Int8) (ha : a ≠ minValue) :
(a / b).toInt64 = a.toInt64 / b.toInt64
source
theorem Int8.toISize_div_of_ne_left (a b : Int8) (ha : a ≠ minValue) :
(a / b).toISize = a.toISize / b.toISize
source
theorem Int16.toInt32_div_of_ne_left (a b : Int16) (ha : a ≠ minValue) :
(a / b).toInt32 = a.toInt32 / b.toInt32
source
theorem Int16.toInt64_div_of_ne_left (a b : Int16) (ha : a ≠ minValue) :
(a / b).toInt64 = a.toInt64 / b.toInt64
source
theorem Int16.toISize_div_of_ne_left (a b : Int16) (ha : a ≠ minValue) :
(a / b).toISize = a.toISize / b.toISize
source
theorem Int32.toInt64_div_of_ne_left (a b : Int32) (ha : a ≠ minValue) :
(a / b).toInt64 = a.toInt64 / b.toInt64
source
theorem Int32.toISize_div_of_ne_left (a b : Int32) (ha : a ≠ minValue) :
(a / b).toISize = a.toISize / b.toISize
source
theorem ISize.toInt64_div_of_ne_left (a b : ISize) (ha : a ≠ minValue) :
(a / b).toInt64 = a.toInt64 / b.toInt64
source
theorem Int8.toInt16_div_of_ne_right (a b : Int8) (hb : b ≠ -1) :
(a / b).toInt16 = a.toInt16 / b.toInt16
source
theorem Int8.toInt32_div_of_ne_right (a b : Int8) (hb : b ≠ -1) :
(a / b).toInt32 = a.toInt32 / b.toInt32
source
theorem Int8.toInt64_div_of_ne_right (a b : Int8) (hb : b ≠ -1) :
(a / b).toInt64 = a.toInt64 / b.toInt64
source
theorem Int8.toISize_div_of_ne_right (a b : Int8) (hb : b ≠ -1) :
(a / b).toISize = a.toISize / b.toISize
source
theorem Int16.toInt32_div_of_ne_right (a b : Int16) (hb : b ≠ -1) :
(a / b).toInt32 = a.toInt32 / b.toInt32
source
theorem Int16.toInt64_div_of_ne_right (a b : Int16) (hb : b ≠ -1) :
(a / b).toInt64 = a.toInt64 / b.toInt64
source
theorem Int16.toISize_div_of_ne_right (a b : Int16) (hb : b ≠ -1) :
(a / b).toISize = a.toISize / b.toISize
source
theorem Int32.toInt64_div_of_ne_right (a b : Int32) (hb : b ≠ -1) :
(a / b).toInt64 = a.toInt64 / b.toInt64
source
theorem Int32.toISize_div_of_ne_right (a b : Int32) (hb : b ≠ -1) :
(a / b).toISize = a.toISize / b.toISize
source
theorem ISize.toInt64_div_of_ne_right (a b : ISize) (hb : b ≠ -1) :
(a / b).toInt64 = a.toInt64 / b.toInt64
source
@[simp]
theorem Int8.minValue_div_neg_one :
minValue / -1 = minValue
source
@[simp]
theorem Int16.minValue_div_neg_one :
minValue / -1 = minValue
source
@[simp]
theorem Int32.minValue_div_neg_one :
minValue / -1 = minValue
source
@[simp]
theorem Int64.minValue_div_neg_one :
minValue / -1 = minValue
source
@[simp]
theorem ISize.minValue_div_neg_one :
minValue / -1 = minValue
source
@[simp]
theorem Int8.toInt_add (a b : Int8) :
(a + b).toInt = (a.toInt + b.toInt).bmod (2 ^ 8)
source
@[simp]
theorem Int16.toInt_add (a b : Int16) :
(a + b).toInt = (a.toInt + b.toInt).bmod (2 ^ 16)
source
@[simp]
theorem Int32.toInt_add (a b : Int32) :
(a + b).toInt = (a.toInt + b.toInt).bmod (2 ^ 32)
source
@[simp]
theorem Int64.toInt_add (a b : Int64) :
(a + b).toInt = (a.toInt + b.toInt).bmod (2 ^ 64)
source
@[simp]
theorem ISize.toInt_add (a b : ISize) :
(a + b).toInt = (a.toInt + b.toInt).bmod (2 ^ System.Platform.numBits)
source
@[simp]
theorem Int16.toInt8_add (a b : Int16) :
(a + b).toInt8 = a.toInt8 + b.toInt8
source
@[simp]
theorem Int32.toInt8_add (a b : Int32) :
(a + b).toInt8 = a.toInt8 + b.toInt8
source
@[simp]
theorem Int32.toInt16_add (a b : Int32) :
(a + b).toInt16 = a.toInt16 + b.toInt16
source
@[simp]
theorem ISize.toInt8_add (a b : ISize) :
(a + b).toInt8 = a.toInt8 + b.toInt8
source
@[simp]
theorem ISize.toInt16_add (a b : ISize) :
(a + b).toInt16 = a.toInt16 + b.toInt16
source
@[simp]
theorem ISize.toInt32_add (a b : ISize) :
(a + b).toInt32 = a.toInt32 + b.toInt32
source
@[simp]
theorem Int64.toInt8_add (a b : Int64) :
(a + b).toInt8 = a.toInt8 + b.toInt8
source
@[simp]
theorem Int64.toInt16_add (a b : Int64) :
(a + b).toInt16 = a.toInt16 + b.toInt16
source
@[simp]
theorem Int64.toInt32_add (a b : Int64) :
(a + b).toInt32 = a.toInt32 + b.toInt32
source
@[simp]
theorem Int64.toISize_add (a b : Int64) :
(a + b).toISize = a.toISize + b.toISize
source
@[simp]
theorem Int8.toInt_mul (a b : Int8) :
(a * b).toInt = (a.toInt * b.toInt).bmod (2 ^ 8)
source
@[simp]
theorem Int16.toInt_mul (a b : Int16) :
(a * b).toInt = (a.toInt * b.toInt).bmod (2 ^ 16)
source
@[simp]
theorem Int32.toInt_mul (a b : Int32) :
(a * b).toInt = (a.toInt * b.toInt).bmod (2 ^ 32)
source
@[simp]
theorem Int64.toInt_mul (a b : Int64) :
(a * b).toInt = (a.toInt * b.toInt).bmod (2 ^ 64)
source
@[simp]
theorem ISize.toInt_mul (a b : ISize) :
(a * b).toInt = (a.toInt * b.toInt).bmod (2 ^ System.Platform.numBits)
source
@[simp]
theorem Int16.toInt8_mul (a b : Int16) :
(a * b).toInt8 = a.toInt8 * b.toInt8
source
@[simp]
theorem Int32.toInt8_mul (a b : Int32) :
(a * b).toInt8 = a.toInt8 * b.toInt8
source
@[simp]
theorem Int32.toInt16_mul (a b : Int32) :
(a * b).toInt16 = a.toInt16 * b.toInt16
source
@[simp]
theorem ISize.toInt8_mul (a b : ISize) :
(a * b).toInt8 = a.toInt8 * b.toInt8
source
@[simp]
theorem ISize.toInt16_mul (a b : ISize) :
(a * b).toInt16 = a.toInt16 * b.toInt16
source
@[simp]
theorem ISize.toInt32_mul (a b : ISize) :
(a * b).toInt32 = a.toInt32 * b.toInt32
source
@[simp]
theorem Int64.toInt8_mul (a b : Int64) :
(a * b).toInt8 = a.toInt8 * b.toInt8
source
@[simp]
theorem Int64.toInt16_mul (a b : Int64) :
(a * b).toInt16 = a.toInt16 * b.toInt16
source
@[simp]
theorem Int64.toInt32_mul (a b : Int64) :
(a * b).toInt32 = a.toInt32 * b.toInt32
source
@[simp]
theorem Int64.toISize_mul (a b : Int64) :
(a * b).toISize = a.toISize * b.toISize
source
theorem Int8.sub_eq_add_neg (a b : Int8) :
a - b = a + -b
source
theorem Int16.sub_eq_add_neg (a b : Int16) :
a - b = a + -b
source
theorem Int32.sub_eq_add_neg (a b : Int32) :
a - b = a + -b
source
theorem Int64.sub_eq_add_neg (a b : Int64) :
a - b = a + -b
source
theorem ISize.sub_eq_add_neg (a b : ISize) :
a - b = a + -b
source
@[simp]
theorem Int8.toInt_sub (a b : Int8) :
(a - b).toInt = (a.toInt - b.toInt).bmod (2 ^ 8)
source
@[simp]
theorem Int16.toInt_sub (a b : Int16) :
(a - b).toInt = (a.toInt - b.toInt).bmod (2 ^ 16)
source
@[simp]
theorem Int32.toInt_sub (a b : Int32) :
(a - b).toInt = (a.toInt - b.toInt).bmod (2 ^ 32)
source
@[simp]
theorem Int64.toInt_sub (a b : Int64) :
(a - b).toInt = (a.toInt - b.toInt).bmod (2 ^ 64)
source
@[simp]
theorem ISize.toInt_sub (a b : ISize) :
(a - b).toInt = (a.toInt - b.toInt).bmod (2 ^ System.Platform.numBits)
source
@[simp]
theorem Int16.toInt8_sub (a b : Int16) :
(a - b).toInt8 = a.toInt8 - b.toInt8
source
@[simp]
theorem Int32.toInt8_sub (a b : Int32) :
(a - b).toInt8 = a.toInt8 - b.toInt8
source
@[simp]
theorem Int32.toInt16_sub (a b : Int32) :
(a - b).toInt16 = a.toInt16 - b.toInt16
source
@[simp]
theorem ISize.toInt8_sub (a b : ISize) :
(a - b).toInt8 = a.toInt8 - b.toInt8
source
@[simp]
theorem ISize.toInt16_sub (a b : ISize) :
(a - b).toInt16 = a.toInt16 - b.toInt16
source
@[simp]
theorem ISize.toInt32_sub (a b : ISize) :
(a - b).toInt32 = a.toInt32 - b.toInt32
source
@[simp]
theorem Int64.toInt8_sub (a b : Int64) :
(a - b).toInt8 = a.toInt8 - b.toInt8
source
@[simp]
theorem Int64.toInt16_sub (a b : Int64) :
(a - b).toInt16 = a.toInt16 - b.toInt16
source
@[simp]
theorem Int64.toInt32_sub (a b : Int64) :
(a - b).toInt32 = a.toInt32 - b.toInt32
source
@[simp]
theorem Int64.toISize_sub (a b : Int64) :
(a - b).toISize = a.toISize - b.toISize
source
@[simp]
theorem Int8.toInt16_lt {a b : Int8} :
a.toInt16 < b.toInt16 ↔ a < b
source
@[simp]
theorem Int8.toInt32_lt {a b : Int8} :
a.toInt32 < b.toInt32 ↔ a < b
source
@[simp]
theorem Int8.toInt64_lt {a b : Int8} :
a.toInt64 < b.toInt64 ↔ a < b
source
@[simp]
theorem Int8.toISize_lt {a b : Int8} :
a.toISize < b.toISize ↔ a < b
source
@[simp]
theorem Int16.toInt32_lt {a b : Int16} :
a.toInt32 < b.toInt32 ↔ a < b
source
@[simp]
theorem Int16.toInt64_lt {a b : Int16} :
a.toInt64 < b.toInt64 ↔ a < b
source
@[simp]
theorem Int16.toISize_lt {a b : Int16} :
a.toISize < b.toISize ↔ a < b
source
@[simp]
theorem Int32.toInt64_lt {a b : Int32} :
a.toInt64 < b.toInt64 ↔ a < b
source
@[simp]
theorem Int32.toISize_lt {a b : Int32} :
a.toISize < b.toISize ↔ a < b
source
@[simp]
theorem ISize.toInt64_lt {a b : ISize} :
a.toInt64 < b.toInt64 ↔ a < b
source
@[simp]
theorem Int8.toInt16_le {a b : Int8} :
a.toInt16 ≤ b.toInt16 ↔ a ≤ b
source
@[simp]
theorem Int8.toInt32_le {a b : Int8} :
a.toInt32 ≤ b.toInt32 ↔ a ≤ b
source
@[simp]
theorem Int8.toInt64_le {a b : Int8} :
a.toInt64 ≤ b.toInt64 ↔ a ≤ b
source
@[simp]
theorem Int8.toISize_le {a b : Int8} :
a.toISize ≤ b.toISize ↔ a ≤ b
source
@[simp]
theorem Int16.toInt32_le {a b : Int16} :
a.toInt32 ≤ b.toInt32 ↔ a ≤ b
source
@[simp]
theorem Int16.toInt64_le {a b : Int16} :
a.toInt64 ≤ b.toInt64 ↔ a ≤ b
source
@[simp]
theorem Int16.toISize_le {a b : Int16} :
a.toISize ≤ b.toISize ↔ a ≤ b
source
@[simp]
theorem Int32.toInt64_le {a b : Int32} :
a.toInt64 ≤ b.toInt64 ↔ a ≤ b
source
@[simp]
theorem Int32.toISize_le {a b : Int32} :
a.toISize ≤ b.toISize ↔ a ≤ b
source
@[simp]
theorem ISize.toInt64_le {a b : ISize} :
a.toInt64 ≤ b.toInt64 ↔ a ≤ b
source
@[simp]
theorem Int8.ofBitVec_neg (a : BitVec 8) :
ofBitVec (-a) = -ofBitVec a
source
@[simp]
theorem Int16.ofBitVec_neg (a : BitVec 16) :
ofBitVec (-a) = -ofBitVec a
source
@[simp]
theorem Int32.ofBitVec_neg (a : BitVec 32) :
ofBitVec (-a) = -ofBitVec a
source
@[simp]
theorem Int64.ofBitVec_neg (a : BitVec 64) :
ofBitVec (-a) = -ofBitVec a
source
@[simp]
theorem ISize.ofBitVec_neg (a : BitVec System.Platform.numBits) :
ofBitVec (-a) = -ofBitVec a
source
@[simp]
theorem Int8.ofInt_neg (a : Int) :
ofInt (-a) = -ofInt a
source
@[simp]
theorem Int16.ofInt_neg (a : Int) :
ofInt (-a) = -ofInt a
source
@[simp]
theorem Int32.ofInt_neg (a : Int) :
ofInt (-a) = -ofInt a
source
@[simp]
theorem Int64.ofInt_neg (a : Int) :
ofInt (-a) = -ofInt a
source
@[simp]
theorem ISize.ofInt_neg (a : Int) :
ofInt (-a) = -ofInt a
source
theorem Int8.ofInt_eq_iff_bmod_eq_toInt (a : Int) (b : Int8) :
ofInt a = b ↔ a.bmod (2 ^ 8) = b.toInt
source
theorem Int16.ofInt_eq_iff_bmod_eq_toInt (a : Int) (b : Int16) :
ofInt a = b ↔ a.bmod (2 ^ 16) = b.toInt
source
theorem Int32.ofInt_eq_iff_bmod_eq_toInt (a : Int) (b : Int32) :
ofInt a = b ↔ a.bmod (2 ^ 32) = b.toInt
source
theorem Int64.ofInt_eq_iff_bmod_eq_toInt (a : Int) (b : Int64) :
ofInt a = b ↔ a.bmod (2 ^ 64) = b.toInt
source
theorem ISize.ofInt_eq_iff_bmod_eq_toInt (a : Int) (b : ISize) :
ofInt a = b ↔ a.bmod (2 ^ System.Platform.numBits) = b.toInt
source
@[simp]
theorem Int8.ofBitVec_add (a b : BitVec 8) :
ofBitVec (a + b) = ofBitVec a + ofBitVec b
source
@[simp]
theorem Int16.ofBitVec_add (a b : BitVec 16) :
ofBitVec (a + b) = ofBitVec a + ofBitVec b
source
@[simp]
theorem Int32.ofBitVec_add (a b : BitVec 32) :
ofBitVec (a + b) = ofBitVec a + ofBitVec b
source
@[simp]
theorem Int64.ofBitVec_add (a b : BitVec 64) :
ofBitVec (a + b) = ofBitVec a + ofBitVec b
source
@[simp]
theorem ISize.ofBitVec_add (a b : BitVec System.Platform.numBits) :
ofBitVec (a + b) = ofBitVec a + ofBitVec b
source
@[simp]
theorem Int8.ofInt_add (a b : Int) :
ofInt (a + b) = ofInt a + ofInt b
source
@[simp]
theorem Int16.ofInt_add (a b : Int) :
ofInt (a + b) = ofInt a + ofInt b
source
@[simp]
theorem Int32.ofInt_add (a b : Int) :
ofInt (a + b) = ofInt a + ofInt b
source
@[simp]
theorem Int64.ofInt_add (a b : Int) :
ofInt (a + b) = ofInt a + ofInt b
source
@[simp]
theorem ISize.ofInt_add (a b : Int) :
ofInt (a + b) = ofInt a + ofInt b
source
@[simp]
theorem Int8.ofNat_add (a b : Nat) :
ofNat (a + b) = ofNat a + ofNat b
source
@[simp]
theorem Int16.ofNat_add (a b : Nat) :
ofNat (a + b) = ofNat a + ofNat b
source
@[simp]
theorem Int32.ofNat_add (a b : Nat) :
ofNat (a + b) = ofNat a + ofNat b
source
@[simp]
theorem Int64.ofNat_add (a b : Nat) :
ofNat (a + b) = ofNat a + ofNat b
source
@[simp]
theorem ISize.ofNat_add (a b : Nat) :
ofNat (a + b) = ofNat a + ofNat b
source
theorem Int8.ofIntLE_add {a b : Int} {hab₁ : minValue.toInt ≤ a + b} {hab₂ : a + b ≤ maxValue.toInt} :
ofIntLE (a + b) hab₁ hab₂ = ofInt a + ofInt b
source
theorem Int16.ofIntLE_add {a b : Int} {hab₁ : minValue.toInt ≤ a + b} {hab₂ : a + b ≤ maxValue.toInt} :
ofIntLE (a + b) hab₁ hab₂ = ofInt a + ofInt b
source
theorem Int32.ofIntLE_add {a b : Int} {hab₁ : minValue.toInt ≤ a + b} {hab₂ : a + b ≤ maxValue.toInt} :
ofIntLE (a + b) hab₁ hab₂ = ofInt a + ofInt b
source
theorem Int64.ofIntLE_add {a b : Int} {hab₁ : minValue.toInt ≤ a + b} {hab₂ : a + b ≤ maxValue.toInt} :
ofIntLE (a + b) hab₁ hab₂ = ofInt a + ofInt b
source
theorem ISize.ofIntLE_add {a b : Int} {hab₁ : minValue.toInt ≤ a + b} {hab₂ : a + b ≤ maxValue.toInt} :
ofIntLE (a + b) hab₁ hab₂ = ofInt a + ofInt b
source
@[simp]
theorem Int8.ofBitVec_sub (a b : BitVec 8) :
ofBitVec (a - b) = ofBitVec a - ofBitVec b
source
@[simp]
theorem Int16.ofBitVec_sub (a b : BitVec 16) :
ofBitVec (a - b) = ofBitVec a - ofBitVec b
source
@[simp]
theorem Int32.ofBitVec_sub (a b : BitVec 32) :
ofBitVec (a - b) = ofBitVec a - ofBitVec b
source
@[simp]
theorem Int64.ofBitVec_sub (a b : BitVec 64) :
ofBitVec (a - b) = ofBitVec a - ofBitVec b
source
@[simp]
theorem ISize.ofBitVec_sub (a b : BitVec System.Platform.numBits) :
ofBitVec (a - b) = ofBitVec a - ofBitVec b
source
@[simp]
theorem Int8.ofInt_sub (a b : Int) :
ofInt (a - b) = ofInt a - ofInt b
source
@[simp]
theorem Int16.ofInt_sub (a b : Int) :
ofInt (a - b) = ofInt a - ofInt b
source
@[simp]
theorem Int32.ofInt_sub (a b : Int) :
ofInt (a - b) = ofInt a - ofInt b
source
@[simp]
theorem Int64.ofInt_sub (a b : Int) :
ofInt (a - b) = ofInt a - ofInt b
source
@[simp]
theorem ISize.ofInt_sub (a b : Int) :
ofInt (a - b) = ofInt a - ofInt b
source
@[simp]
theorem Int8.ofNat_sub (a b : Nat) (hab : b ≤ a) :
ofNat (a - b) = ofNat a - ofNat b
source
@[simp]
theorem Int16.ofNat_sub (a b : Nat) (hab : b ≤ a) :
ofNat (a - b) = ofNat a - ofNat b
source
@[simp]
theorem Int32.ofNat_sub (a b : Nat) (hab : b ≤ a) :
ofNat (a - b) = ofNat a - ofNat b
source
@[simp]
theorem Int64.ofNat_sub (a b : Nat) (hab : b ≤ a) :
ofNat (a - b) = ofNat a - ofNat b
source
@[simp]
theorem ISize.ofNat_sub (a b : Nat) (hab : b ≤ a) :
ofNat (a - b) = ofNat a - ofNat b
source
theorem Int8.ofIntLE_sub {a b : Int} {hab₁ : minValue.toInt ≤ a - b} {hab₂ : a - b ≤ maxValue.toInt} :
ofIntLE (a - b) hab₁ hab₂ = ofInt a - ofInt b
source
theorem Int16.ofIntLE_sub {a b : Int} {hab₁ : minValue.toInt ≤ a - b} {hab₂ : a - b ≤ maxValue.toInt} :
ofIntLE (a - b) hab₁ hab₂ = ofInt a - ofInt b
source
theorem Int32.ofIntLE_sub {a b : Int} {hab₁ : minValue.toInt ≤ a - b} {hab₂ : a - b ≤ maxValue.toInt} :
ofIntLE (a - b) hab₁ hab₂ = ofInt a - ofInt b
source
theorem Int64.ofIntLE_sub {a b : Int} {hab₁ : minValue.toInt ≤ a - b} {hab₂ : a - b ≤ maxValue.toInt} :
ofIntLE (a - b) hab₁ hab₂ = ofInt a - ofInt b
source
theorem ISize.ofIntLE_sub {a b : Int} {hab₁ : minValue.toInt ≤ a - b} {hab₂ : a - b ≤ maxValue.toInt} :
ofIntLE (a - b) hab₁ hab₂ = ofInt a - ofInt b
source
@[simp]
theorem Int8.ofBitVec_mul (a b : BitVec 8) :
ofBitVec (a * b) = ofBitVec a * ofBitVec b
source
@[simp]
theorem Int16.ofBitVec_mul (a b : BitVec 16) :
ofBitVec (a * b) = ofBitVec a * ofBitVec b
source
@[simp]
theorem Int32.ofBitVec_mul (a b : BitVec 32) :
ofBitVec (a * b) = ofBitVec a * ofBitVec b
source
@[simp]
theorem Int64.ofBitVec_mul (a b : BitVec 64) :
ofBitVec (a * b) = ofBitVec a * ofBitVec b
source
@[simp]
theorem ISize.ofBitVec_mul (a b : BitVec System.Platform.numBits) :
ofBitVec (a * b) = ofBitVec a * ofBitVec b
source
@[simp]
theorem Int8.ofInt_mul (a b : Int) :
ofInt (a * b) = ofInt a * ofInt b
source
@[simp]
theorem Int16.ofInt_mul (a b : Int) :
ofInt (a * b) = ofInt a * ofInt b
source
@[simp]
theorem Int32.ofInt_mul (a b : Int) :
ofInt (a * b) = ofInt a * ofInt b
source
@[simp]
theorem Int64.ofInt_mul (a b : Int) :
ofInt (a * b) = ofInt a * ofInt b
source
@[simp]
theorem ISize.ofInt_mul (a b : Int) :
ofInt (a * b) = ofInt a * ofInt b
source
@[simp]
theorem Int8.ofNat_mul (a b : Nat) :
ofNat (a * b) = ofNat a * ofNat b
source
@[simp]
theorem Int16.ofNat_mul (a b : Nat) :
ofNat (a * b) = ofNat a * ofNat b
source
@[simp]
theorem Int32.ofNat_mul (a b : Nat) :
ofNat (a * b) = ofNat a * ofNat b
source
@[simp]
theorem Int64.ofNat_mul (a b : Nat) :
ofNat (a * b) = ofNat a * ofNat b
source
@[simp]
theorem ISize.ofNat_mul (a b : Nat) :
ofNat (a * b) = ofNat a * ofNat b
source
theorem Int8.ofIntLE_mul {a b : Int} {hab₁ : minValue.toInt ≤ a * b} {hab₂ : a * b ≤ maxValue.toInt} :
ofIntLE (a * b) hab₁ hab₂ = ofInt a * ofInt b
source
theorem Int16.ofIntLE_mul {a b : Int} {hab₁ : minValue.toInt ≤ a * b} {hab₂ : a * b ≤ maxValue.toInt} :
ofIntLE (a * b) hab₁ hab₂ = ofInt a * ofInt b
source
theorem Int32.ofIntLE_mul {a b : Int} {hab₁ : minValue.toInt ≤ a * b} {hab₂ : a * b ≤ maxValue.toInt} :
ofIntLE (a * b) hab₁ hab₂ = ofInt a * ofInt b
source
theorem Int64.ofIntLE_mul {a b : Int} {hab₁ : minValue.toInt ≤ a * b} {hab₂ : a * b ≤ maxValue.toInt} :
ofIntLE (a * b) hab₁ hab₂ = ofInt a * ofInt b
source
theorem ISize.ofIntLE_mul {a b : Int} {hab₁ : minValue.toInt ≤ a * b} {hab₂ : a * b ≤ maxValue.toInt} :
ofIntLE (a * b) hab₁ hab₂ = ofInt a * ofInt b
source
theorem Int8.toInt_minValue_lt_zero :
minValue.toInt < 0
source
theorem Int16.toInt_minValue_lt_zero :
minValue.toInt < 0
source
theorem Int32.toInt_minValue_lt_zero :
minValue.toInt < 0
source
theorem Int64.toInt_minValue_lt_zero :
minValue.toInt < 0
source
theorem ISize.toInt_minValue_lt_zero :
minValue.toInt < 0
source
theorem Int8.toInt_maxValue_add_one :
maxValue.toInt + 1 = 2 ^ 7
source
theorem Int16.toInt_maxValue_add_one :
maxValue.toInt + 1 = 2 ^ 15
source
theorem Int32.toInt_maxValue_add_one :
maxValue.toInt + 1 = 2 ^ 31
source
theorem Int64.toInt_maxValue_add_one :
maxValue.toInt + 1 = 2 ^ 63
source
theorem ISize.toInt_maxValue_add_one :
maxValue.toInt + 1 = 2 ^ (System.Platform.numBits - 1)
source
@[simp]
theorem Int8.ofBitVec_sdiv (a b : BitVec 8) :
ofBitVec (a.sdiv b) = ofBitVec a / ofBitVec b
source
@[simp]
theorem Int16.ofBitVec_sdiv (a b : BitVec 16) :
ofBitVec (a.sdiv b) = ofBitVec a / ofBitVec b
source
@[simp]
theorem Int32.ofBitVec_sdiv (a b : BitVec 32) :
ofBitVec (a.sdiv b) = ofBitVec a / ofBitVec b
source
@[simp]
theorem Int64.ofBitVec_sdiv (a b : BitVec 64) :
ofBitVec (a.sdiv b) = ofBitVec a / ofBitVec b
source
@[simp]
theorem ISize.ofBitVec_sdiv (a b : BitVec System.Platform.numBits) :
ofBitVec (a.sdiv b) = ofBitVec a / ofBitVec b
source
theorem Int8.ofInt_tdiv {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) :
ofInt (a.tdiv b) = ofInt a / ofInt b
source
theorem Int16.ofInt_tdiv {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) :
ofInt (a.tdiv b) = ofInt a / ofInt b
source
theorem Int32.ofInt_tdiv {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) :
ofInt (a.tdiv b) = ofInt a / ofInt b
source
theorem Int64.ofInt_tdiv {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) :
ofInt (a.tdiv b) = ofInt a / ofInt b
source
theorem ISize.ofInt_tdiv {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) :
ofInt (a.tdiv b) = ofInt a / ofInt b
source
theorem Int8.ofInt_eq_ofIntLE_div {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) :
ofInt (a.tdiv b) = ofIntLE a ha₁ ha₂ / ofIntLE b hb₁ hb₂
source
theorem Int16.ofInt_eq_ofIntLE_div {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) :
ofInt (a.tdiv b) = ofIntLE a ha₁ ha₂ / ofIntLE b hb₁ hb₂
source
theorem Int32.ofInt_eq_ofIntLE_div {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) :
ofInt (a.tdiv b) = ofIntLE a ha₁ ha₂ / ofIntLE b hb₁ hb₂
source
theorem Int64.ofInt_eq_ofIntLE_div {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) :
ofInt (a.tdiv b) = ofIntLE a ha₁ ha₂ / ofIntLE b hb₁ hb₂
source
theorem ISize.ofInt_eq_ofIntLE_div {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) :
ofInt (a.tdiv b) = ofIntLE a ha₁ ha₂ / ofIntLE b hb₁ hb₂
source
theorem Int8.ofNat_div {a b : Nat} (ha : a < 2 ^ 7) (hb : b < 2 ^ 7) :
ofNat (a / b) = ofNat a / ofNat b
source
theorem Int16.ofNat_div {a b : Nat} (ha : a < 2 ^ 15) (hb : b < 2 ^ 15) :
ofNat (a / b) = ofNat a / ofNat b
source
theorem Int32.ofNat_div {a b : Nat} (ha : a < 2 ^ 31) (hb : b < 2 ^ 31) :
ofNat (a / b) = ofNat a / ofNat b
source
theorem Int64.ofNat_div {a b : Nat} (ha : a < 2 ^ 63) (hb : b < 2 ^ 63) :
ofNat (a / b) = ofNat a / ofNat b
source
theorem ISize.ofNat_div {a b : Nat} (ha : a < 2 ^ (System.Platform.numBits - 1)) (hb : b < 2 ^ (System.Platform.numBits - 1)) :
ofNat (a / b) = ofNat a / ofNat b
source
@[simp]
theorem Int8.ofBitVec_srem (a b : BitVec 8) :
ofBitVec (a.srem b) = ofBitVec a % ofBitVec b
source
@[simp]
theorem Int16.ofBitVec_srem (a b : BitVec 16) :
ofBitVec (a.srem b) = ofBitVec a % ofBitVec b
source
@[simp]
theorem Int32.ofBitVec_srem (a b : BitVec 32) :
ofBitVec (a.srem b) = ofBitVec a % ofBitVec b
source
@[simp]
theorem Int64.ofBitVec_srem (a b : BitVec 64) :
ofBitVec (a.srem b) = ofBitVec a % ofBitVec b
source
@[simp]
theorem ISize.ofBitVec_srem (a b : BitVec System.Platform.numBits) :
ofBitVec (a.srem b) = ofBitVec a % ofBitVec b
source
@[simp]
theorem Int8.toInt_bmod_size (a : Int8) :
a.toInt.bmod size = a.toInt
source
@[simp]
theorem Int16.toInt_bmod_size (a : Int16) :
a.toInt.bmod size = a.toInt
source
@[simp]
theorem Int32.toInt_bmod_size (a : Int32) :
a.toInt.bmod size = a.toInt
source
@[simp]
theorem Int64.toInt_bmod_size (a : Int64) :
a.toInt.bmod size = a.toInt
source
@[simp]
theorem ISize.toInt_bmod_size (a : ISize) :
a.toInt.bmod size = a.toInt
source
theorem Int8.ofIntLE_le_iff_le {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) :
ofIntLE a ha₁ ha₂ ≤ ofIntLE b hb₁ hb₂ ↔ a ≤ b
source
theorem Int16.ofIntLE_le_iff_le {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) :
ofIntLE a ha₁ ha₂ ≤ ofIntLE b hb₁ hb₂ ↔ a ≤ b
source
theorem Int32.ofIntLE_le_iff_le {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) :
ofIntLE a ha₁ ha₂ ≤ ofIntLE b hb₁ hb₂ ↔ a ≤ b
source
theorem Int64.ofIntLE_le_iff_le {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) :
ofIntLE a ha₁ ha₂ ≤ ofIntLE b hb₁ hb₂ ↔ a ≤ b
source
theorem ISize.ofIntLE_le_iff_le {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) :
ofIntLE a ha₁ ha₂ ≤ ofIntLE b hb₁ hb₂ ↔ a ≤ b
source
theorem Int8.ofInt_le_iff_le {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) :
ofInt a ≤ ofInt b ↔ a ≤ b
source
theorem Int16.ofInt_le_iff_le {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) :
ofInt a ≤ ofInt b ↔ a ≤ b
source
theorem Int32.ofInt_le_iff_le {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) :
ofInt a ≤ ofInt b ↔ a ≤ b
source
theorem Int64.ofInt_le_iff_le {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) :
ofInt a ≤ ofInt b ↔ a ≤ b
source
theorem ISize.ofInt_le_iff_le {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) :
ofInt a ≤ ofInt b ↔ a ≤ b
source
theorem Int8.ofNat_le_iff_le {a b : Nat} (ha : a < 2 ^ 7) (hb : b < 2 ^ 7) :
ofNat a ≤ ofNat b ↔ a ≤ b
source
theorem Int16.ofNat_le_iff_le {a b : Nat} (ha : a < 2 ^ 15) (hb : b < 2 ^ 15) :
ofNat a ≤ ofNat b ↔ a ≤ b
source
theorem Int32.ofNat_le_iff_le {a b : Nat} (ha : a < 2 ^ 31) (hb : b < 2 ^ 31) :
ofNat a ≤ ofNat b ↔ a ≤ b
source
theorem Int64.ofNat_le_iff_le {a b : Nat} (ha : a < 2 ^ 63) (hb : b < 2 ^ 63) :
ofNat a ≤ ofNat b ↔ a ≤ b
source
theorem ISize.ofNat_le_iff_le {a b : Nat} (ha : a < 2 ^ (System.Platform.numBits - 1)) (hb : b < 2 ^ (System.Platform.numBits - 1)) :
ofNat a ≤ ofNat b ↔ a ≤ b
source
theorem Int8.ofBitVec_le_iff_sle (a b : BitVec 8) :
ofBitVec a ≤ ofBitVec b ↔ a.sle b = true
source
theorem Int16.ofBitVec_le_iff_sle (a b : BitVec 16) :
ofBitVec a ≤ ofBitVec b ↔ a.sle b = true
source
theorem Int32.ofBitVec_le_iff_sle (a b : BitVec 32) :
ofBitVec a ≤ ofBitVec b ↔ a.sle b = true
source
theorem Int64.ofBitVec_le_iff_sle (a b : BitVec 64) :
ofBitVec a ≤ ofBitVec b ↔ a.sle b = true
source
theorem ISize.ofBitVec_le_iff_sle (a b : BitVec System.Platform.numBits) :
ofBitVec a ≤ ofBitVec b ↔ a.sle b = true
source
theorem Int8.ofIntLE_lt_iff_lt {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) :
ofIntLE a ha₁ ha₂ < ofIntLE b hb₁ hb₂ ↔ a < b
source
theorem Int16.ofIntLE_lt_iff_lt {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) :
ofIntLE a ha₁ ha₂ < ofIntLE b hb₁ hb₂ ↔ a < b
source
theorem Int32.ofIntLE_lt_iff_lt {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) :
ofIntLE a ha₁ ha₂ < ofIntLE b hb₁ hb₂ ↔ a < b
source
theorem Int64.ofIntLE_lt_iff_lt {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) :
ofIntLE a ha₁ ha₂ < ofIntLE b hb₁ hb₂ ↔ a < b
source
theorem ISize.ofIntLE_lt_iff_lt {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) :
ofIntLE a ha₁ ha₂ < ofIntLE b hb₁ hb₂ ↔ a < b
source
theorem Int8.ofInt_lt_iff_lt {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) :
ofInt a < ofInt b ↔ a < b
source
theorem Int16.ofInt_lt_iff_lt {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) :
ofInt a < ofInt b ↔ a < b
source
theorem Int32.ofInt_lt_iff_lt {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) :
ofInt a < ofInt b ↔ a < b
source
theorem Int64.ofInt_lt_iff_lt {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) :
ofInt a < ofInt b ↔ a < b
source
theorem ISize.ofInt_lt_iff_lt {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) :
ofInt a < ofInt b ↔ a < b
source
theorem Int8.ofNat_lt_iff_lt {a b : Nat} (ha : a < 2 ^ 7) (hb : b < 2 ^ 7) :
ofNat a < ofNat b ↔ a < b
source
theorem Int16.ofNat_lt_iff_lt {a b : Nat} (ha : a < 2 ^ 15) (hb : b < 2 ^ 15) :
ofNat a < ofNat b ↔ a < b
source
theorem Int32.ofNat_lt_iff_lt {a b : Nat} (ha : a < 2 ^ 31) (hb : b < 2 ^ 31) :
ofNat a < ofNat b ↔ a < b
source
theorem Int64.ofNat_lt_iff_lt {a b : Nat} (ha : a < 2 ^ 63) (hb : b < 2 ^ 63) :
ofNat a < ofNat b ↔ a < b
source
theorem ISize.ofNat_lt_iff_lt {a b : Nat} (ha : a < 2 ^ (System.Platform.numBits - 1)) (hb : b < 2 ^ (System.Platform.numBits - 1)) :
ofNat a < ofNat b ↔ a < b
source
theorem Int8.ofBitVec_lt_iff_slt (a b : BitVec 8) :
ofBitVec a < ofBitVec b ↔ a.slt b = true
source
theorem Int16.ofBitVec_lt_iff_slt (a b : BitVec 16) :
ofBitVec a < ofBitVec b ↔ a.slt b = true
source
theorem Int32.ofBitVec_lt_iff_slt (a b : BitVec 32) :
ofBitVec a < ofBitVec b ↔ a.slt b = true
source
theorem Int64.ofBitVec_lt_iff_slt (a b : BitVec 64) :
ofBitVec a < ofBitVec b ↔ a.slt b = true
source
theorem ISize.ofBitVec_lt_iff_slt (a b : BitVec System.Platform.numBits) :
ofBitVec a < ofBitVec b ↔ a.slt b = true
source
theorem Int8.toNatClampNeg_one :
toNatClampNeg 1 = 1
source
theorem Int16.toNatClampNeg_one :
toNatClampNeg 1 = 1
source
theorem Int32.toNatClampNeg_one :
toNatClampNeg 1 = 1
source
theorem Int64.toNatClampNeg_one :
toNatClampNeg 1 = 1
source
theorem ISize.toNatClampNeg_one :
toNatClampNeg 1 = 1
source
theorem Int8.toInt_one :
toInt 1 = 1
source
theorem Int16.toInt_one :
toInt 1 = 1
source
theorem Int32.toInt_one :
toInt 1 = 1
source
theorem Int64.toInt_one :
toInt 1 = 1
source
theorem ISize.toInt_one :
toInt 1 = 1
source
theorem Int8.zero_lt_one :
0 < 1
source
theorem Int16.zero_lt_one :
0 < 1
source
theorem Int32.zero_lt_one :
0 < 1
source
theorem Int64.zero_lt_one :
0 < 1
source
theorem ISize.zero_lt_one :
0 < 1
source
theorem Int8.zero_ne_one :
0 ≠ 1
source
theorem Int16.zero_ne_one :
0 ≠ 1
source
theorem Int32.zero_ne_one :
0 ≠ 1
source
theorem Int64.zero_ne_one :
0 ≠ 1
source
theorem ISize.zero_ne_one :
0 ≠ 1
source
theorem Int8.add_assoc (a b c : Int8) :
a + b + c = a + (b + c)
source
theorem Int16.add_assoc (a b c : Int16) :
a + b + c = a + (b + c)
source
theorem Int32.add_assoc (a b c : Int32) :
a + b + c = a + (b + c)
source
theorem Int64.add_assoc (a b c : Int64) :
a + b + c = a + (b + c)
source
theorem ISize.add_assoc (a b c : ISize) :
a + b + c = a + (b + c)
source
instance instAssociativeInt8HAdd :
Std.Associative fun (x1 x2 : Int8) => x1 + x2
source
instance instAssociativeInt16HAdd :
Std.Associative fun (x1 x2 : Int16) => x1 + x2
source
instance instAssociativeInt32HAdd :
Std.Associative fun (x1 x2 : Int32) => x1 + x2
source
instance instAssociativeInt64HAdd :
Std.Associative fun (x1 x2 : Int64) => x1 + x2
source
instance instAssociativeISizeHAdd :
Std.Associative fun (x1 x2 : ISize) => x1 + x2
source
theorem Int8.add_comm (a b : Int8) :
a + b = b + a
source
theorem Int16.add_comm (a b : Int16) :
a + b = b + a
source
theorem Int32.add_comm (a b : Int32) :
a + b = b + a
source
theorem Int64.add_comm (a b : Int64) :
a + b = b + a
source
theorem ISize.add_comm (a b : ISize) :
a + b = b + a
source
instance instCommutativeInt8HAdd :
Std.Commutative fun (x1 x2 : Int8) => x1 + x2
source
instance instCommutativeInt16HAdd :
Std.Commutative fun (x1 x2 : Int16) => x1 + x2
source
instance instCommutativeInt32HAdd :
Std.Commutative fun (x1 x2 : Int32) => x1 + x2
source
instance instCommutativeInt64HAdd :
Std.Commutative fun (x1 x2 : Int64) => x1 + x2
source
instance instCommutativeISizeHAdd :
Std.Commutative fun (x1 x2 : ISize) => x1 + x2
source
@[simp]
theorem Int8.add_zero (a : Int8) :
a + 0 = a
source
@[simp]
theorem Int16.add_zero (a : Int16) :
a + 0 = a
source
@[simp]
theorem Int32.add_zero (a : Int32) :
a + 0 = a
source
@[simp]
theorem Int64.add_zero (a : Int64) :
a + 0 = a
source
@[simp]
theorem ISize.add_zero (a : ISize) :
a + 0 = a
source
@[simp]
theorem Int8.zero_add (a : Int8) :
0 + a = a
source
@[simp]
theorem Int16.zero_add (a : Int16) :
0 + a = a
source
@[simp]
theorem Int32.zero_add (a : Int32) :
0 + a = a
source
@[simp]
theorem Int64.zero_add (a : Int64) :
0 + a = a
source
@[simp]
theorem ISize.zero_add (a : ISize) :
0 + a = a
source
instance instLawfulIdentityInt8HAddOfNat :
Std.LawfulIdentity (fun (x1 x2 : Int8) => x1 + x2) 0
source
instance instLawfulIdentityInt16HAddOfNat :
Std.LawfulIdentity (fun (x1 x2 : Int16) => x1 + x2) 0
source
instance instLawfulIdentityInt32HAddOfNat :
Std.LawfulIdentity (fun (x1 x2 : Int32) => x1 + x2) 0
source
instance instLawfulIdentityInt64HAddOfNat :
Std.LawfulIdentity (fun (x1 x2 : Int64) => x1 + x2) 0
source
instance instLawfulIdentityISizeHAddOfNat :
Std.LawfulIdentity (fun (x1 x2 : ISize) => x1 + x2) 0
source
@[simp]
theorem Int8.sub_zero (a : Int8) :
a - 0 = a
source
@[simp]
theorem Int16.sub_zero (a : Int16) :
a - 0 = a
source
@[simp]
theorem Int32.sub_zero (a : Int32) :
a - 0 = a
source
@[simp]
theorem Int64.sub_zero (a : Int64) :
a - 0 = a
source
@[simp]
theorem ISize.sub_zero (a : ISize) :
a - 0 = a
source
@[simp]
theorem Int8.zero_sub (a : Int8) :
0 - a = -a
source
@[simp]
theorem Int16.zero_sub (a : Int16) :
0 - a = -a
source
@[simp]
theorem Int32.zero_sub (a : Int32) :
0 - a = -a
source
@[simp]
theorem Int64.zero_sub (a : Int64) :
0 - a = -a
source
@[simp]
theorem ISize.zero_sub (a : ISize) :
0 - a = -a
source
@[simp]
theorem Int8.sub_self (a : Int8) :
a - a = 0
source
@[simp]
theorem Int16.sub_self (a : Int16) :
a - a = 0
source
@[simp]
theorem Int32.sub_self (a : Int32) :
a - a = 0
source
@[simp]
theorem Int64.sub_self (a : Int64) :
a - a = 0
source
@[simp]
theorem ISize.sub_self (a : ISize) :
a - a = 0
source
theorem Int8.add_left_neg (a : Int8) :
-a + a = 0
source
theorem Int8.add_right_neg (a : Int8) :
a + -a = 0
source
theorem Int16.add_left_neg (a : Int16) :
-a + a = 0
source
theorem Int16.add_right_neg (a : Int16) :
a + -a = 0
source
theorem Int32.add_left_neg (a : Int32) :
-a + a = 0
source
theorem Int32.add_right_neg (a : Int32) :
a + -a = 0
source
theorem Int64.add_left_neg (a : Int64) :
-a + a = 0
source
theorem Int64.add_right_neg (a : Int64) :
a + -a = 0
source
theorem ISize.add_left_neg (a : ISize) :
-a + a = 0
source
theorem ISize.add_right_neg (a : ISize) :
a + -a = 0
source
@[simp]
theorem Int8.sub_add_cancel (a b : Int8) :
a - b + b = a
source
@[simp]
theorem Int16.sub_add_cancel (a b : Int16) :
a - b + b = a
source
@[simp]
theorem Int32.sub_add_cancel (a b : Int32) :
a - b + b = a
source
@[simp]
theorem Int64.sub_add_cancel (a b : Int64) :
a - b + b = a
source
@[simp]
theorem ISize.sub_add_cancel (a b : ISize) :
a - b + b = a
source
theorem Int8.eq_sub_iff_add_eq {a b c : Int8} :
a = c - b ↔ a + b = c
source
theorem Int16.eq_sub_iff_add_eq {a b c : Int16} :
a = c - b ↔ a + b = c
source
theorem Int32.eq_sub_iff_add_eq {a b c : Int32} :
a = c - b ↔ a + b = c
source
theorem Int64.eq_sub_iff_add_eq {a b c : Int64} :
a = c - b ↔ a + b = c
source
theorem ISize.eq_sub_iff_add_eq {a b c : ISize} :
a = c - b ↔ a + b = c
source
theorem Int8.sub_eq_iff_eq_add {a b c : Int8} :
a - b = c ↔ a = c + b
source
theorem Int16.sub_eq_iff_eq_add {a b c : Int16} :
a - b = c ↔ a = c + b
source
theorem Int32.sub_eq_iff_eq_add {a b c : Int32} :
a - b = c ↔ a = c + b
source
theorem Int64.sub_eq_iff_eq_add {a b c : Int64} :
a - b = c ↔ a = c + b
source
theorem ISize.sub_eq_iff_eq_add {a b c : ISize} :
a - b = c ↔ a = c + b
source
@[simp]
theorem Int8.neg_neg {a : Int8} :
- -a = a
source
@[simp]
theorem Int16.neg_neg {a : Int16} :
- -a = a
source
@[simp]
theorem Int32.neg_neg {a : Int32} :
- -a = a
source
@[simp]
theorem Int64.neg_neg {a : Int64} :
- -a = a
source
@[simp]
theorem ISize.neg_neg {a : ISize} :
- -a = a
source
@[simp]
theorem Int8.neg_inj {a b : Int8} :
-a = -b ↔ a = b
source
@[simp]
theorem Int16.neg_inj {a b : Int16} :
-a = -b ↔ a = b
source
@[simp]
theorem Int32.neg_inj {a b : Int32} :
-a = -b ↔ a = b
source
@[simp]
theorem Int64.neg_inj {a b : Int64} :
-a = -b ↔ a = b
source
@[simp]
theorem ISize.neg_inj {a b : ISize} :
-a = -b ↔ a = b
source
@[simp]
theorem Int8.neg_ne_zero {a : Int8} :
-a ≠ 0 ↔ a ≠ 0
source
@[simp]
theorem Int16.neg_ne_zero {a : Int16} :
-a ≠ 0 ↔ a ≠ 0
source
@[simp]
theorem Int32.neg_ne_zero {a : Int32} :
-a ≠ 0 ↔ a ≠ 0
source
@[simp]
theorem Int64.neg_ne_zero {a : Int64} :
-a ≠ 0 ↔ a ≠ 0
source
@[simp]
theorem ISize.neg_ne_zero {a : ISize} :
-a ≠ 0 ↔ a ≠ 0
source
theorem Int8.neg_add {a b : Int8} :
-(a + b) = -a - b
source
theorem Int16.neg_add {a b : Int16} :
-(a + b) = -a - b
source
theorem Int32.neg_add {a b : Int32} :
-(a + b) = -a - b
source
theorem Int64.neg_add {a b : Int64} :
-(a + b) = -a - b
source
theorem ISize.neg_add {a b : ISize} :
-(a + b) = -a - b
source
@[simp]
theorem Int8.sub_neg {a b : Int8} :
a - -b = a + b
source
@[simp]
theorem Int16.sub_neg {a b : Int16} :
a - -b = a + b
source
@[simp]
theorem Int32.sub_neg {a b : Int32} :
a - -b = a + b
source
@[simp]
theorem Int64.sub_neg {a b : Int64} :
a - -b = a + b
source
@[simp]
theorem ISize.sub_neg {a b : ISize} :
a - -b = a + b
source
@[simp]
theorem Int8.neg_sub {a b : Int8} :
-(a - b) = b - a
source
@[simp]
theorem Int16.neg_sub {a b : Int16} :
-(a - b) = b - a
source
@[simp]
theorem Int32.neg_sub {a b : Int32} :
-(a - b) = b - a
source
@[simp]
theorem Int64.neg_sub {a b : Int64} :
-(a - b) = b - a
source
@[simp]
theorem ISize.neg_sub {a b : ISize} :
-(a - b) = b - a
source
theorem Int8.sub_sub (a b c : Int8) :
a - b - c = a - (b + c)
source
theorem Int16.sub_sub (a b c : Int16) :
a - b - c = a - (b + c)
source
theorem Int32.sub_sub (a b c : Int32) :
a - b - c = a - (b + c)
source
theorem Int64.sub_sub (a b c : Int64) :
a - b - c = a - (b + c)
source
theorem ISize.sub_sub (a b c : ISize) :
a - b - c = a - (b + c)
source
@[simp]
theorem Int8.add_left_inj {a b : Int8} (c : Int8) :
a + c = b + c ↔ a = b
source
@[simp]
theorem Int16.add_left_inj {a b : Int16} (c : Int16) :
a + c = b + c ↔ a = b
source
@[simp]
theorem Int32.add_left_inj {a b : Int32} (c : Int32) :
a + c = b + c ↔ a = b
source
@[simp]
theorem Int64.add_left_inj {a b : Int64} (c : Int64) :
a + c = b + c ↔ a = b
source
@[simp]
theorem ISize.add_left_inj {a b : ISize} (c : ISize) :
a + c = b + c ↔ a = b
source
@[simp]
theorem Int8.add_right_inj {a b : Int8} (c : Int8) :
c + a = c + b ↔ a = b
source
@[simp]
theorem Int16.add_right_inj {a b : Int16} (c : Int16) :
c + a = c + b ↔ a = b
source
@[simp]
theorem Int32.add_right_inj {a b : Int32} (c : Int32) :
c + a = c + b ↔ a = b
source
@[simp]
theorem Int64.add_right_inj {a b : Int64} (c : Int64) :
c + a = c + b ↔ a = b
source
@[simp]
theorem ISize.add_right_inj {a b : ISize} (c : ISize) :
c + a = c + b ↔ a = b
source
@[simp]
theorem Int8.sub_left_inj {a b : Int8} (c : Int8) :
a - c = b - c ↔ a = b
source
@[simp]
theorem Int16.sub_left_inj {a b : Int16} (c : Int16) :
a - c = b - c ↔ a = b
source
@[simp]
theorem Int32.sub_left_inj {a b : Int32} (c : Int32) :
a - c = b - c ↔ a = b
source
@[simp]
theorem Int64.sub_left_inj {a b : Int64} (c : Int64) :
a - c = b - c ↔ a = b
source
@[simp]
theorem ISize.sub_left_inj {a b : ISize} (c : ISize) :
a - c = b - c ↔ a = b
source
@[simp]
theorem Int8.sub_right_inj {a b : Int8} (c : Int8) :
c - a = c - b ↔ a = b
source
@[simp]
theorem Int16.sub_right_inj {a b : Int16} (c : Int16) :
c - a = c - b ↔ a = b
source
@[simp]
theorem Int32.sub_right_inj {a b : Int32} (c : Int32) :
c - a = c - b ↔ a = b
source
@[simp]
theorem Int64.sub_right_inj {a b : Int64} (c : Int64) :
c - a = c - b ↔ a = b
source
@[simp]
theorem ISize.sub_right_inj {a b : ISize} (c : ISize) :
c - a = c - b ↔ a = b
source
@[simp]
theorem Int8.add_eq_right {a b : Int8} :
a + b = b ↔ a = 0
source
@[simp]
theorem Int16.add_eq_right {a b : Int16} :
a + b = b ↔ a = 0
source
@[simp]
theorem Int32.add_eq_right {a b : Int32} :
a + b = b ↔ a = 0
source
@[simp]
theorem Int64.add_eq_right {a b : Int64} :
a + b = b ↔ a = 0
source
@[simp]
theorem ISize.add_eq_right {a b : ISize} :
a + b = b ↔ a = 0
source
@[simp]
theorem Int8.add_eq_left {a b : Int8} :
a + b = a ↔ b = 0
source
@[simp]
theorem Int16.add_eq_left {a b : Int16} :
a + b = a ↔ b = 0
source
@[simp]
theorem Int32.add_eq_left {a b : Int32} :
a + b = a ↔ b = 0
source
@[simp]
theorem Int64.add_eq_left {a b : Int64} :
a + b = a ↔ b = 0
source
@[simp]
theorem ISize.add_eq_left {a b : ISize} :
a + b = a ↔ b = 0
source
@[simp]
theorem Int8.right_eq_add {a b : Int8} :
b = a + b ↔ a = 0
source
@[simp]
theorem Int16.right_eq_add {a b : Int16} :
b = a + b ↔ a = 0
source
@[simp]
theorem Int32.right_eq_add {a b : Int32} :
b = a + b ↔ a = 0
source
@[simp]
theorem Int64.right_eq_add {a b : Int64} :
b = a + b ↔ a = 0
source
@[simp]
theorem ISize.right_eq_add {a b : ISize} :
b = a + b ↔ a = 0
source
@[simp]
theorem Int8.left_eq_add {a b : Int8} :
a = a + b ↔ b = 0
source
@[simp]
theorem Int16.left_eq_add {a b : Int16} :
a = a + b ↔ b = 0
source
@[simp]
theorem Int32.left_eq_add {a b : Int32} :
a = a + b ↔ b = 0
source
@[simp]
theorem Int64.left_eq_add {a b : Int64} :
a = a + b ↔ b = 0
source
@[simp]
theorem ISize.left_eq_add {a b : ISize} :
a = a + b ↔ b = 0
source
theorem Int8.mul_comm (a b : Int8) :
a * b = b * a
source
theorem Int16.mul_comm (a b : Int16) :
a * b = b * a
source
theorem Int32.mul_comm (a b : Int32) :
a * b = b * a
source
theorem Int64.mul_comm (a b : Int64) :
a * b = b * a
source
theorem ISize.mul_comm (a b : ISize) :
a * b = b * a
source
instance instCommutativeInt8HMul :
Std.Commutative fun (x1 x2 : Int8) => x1 * x2
source
instance instCommutativeInt16HMul :
Std.Commutative fun (x1 x2 : Int16) => x1 * x2
source
instance instCommutativeInt32HMul :
Std.Commutative fun (x1 x2 : Int32) => x1 * x2
source
instance instCommutativeInt64HMul :
Std.Commutative fun (x1 x2 : Int64) => x1 * x2
source
instance instCommutativeISizeHMul :
Std.Commutative fun (x1 x2 : ISize) => x1 * x2
source
theorem Int8.mul_assoc (a b c : Int8) :
a * b * c = a * (b * c)
source
theorem Int16.mul_assoc (a b c : Int16) :
a * b * c = a * (b * c)
source
theorem Int32.mul_assoc (a b c : Int32) :
a * b * c = a * (b * c)
source
theorem Int64.mul_assoc (a b c : Int64) :
a * b * c = a * (b * c)
source
theorem ISize.mul_assoc (a b c : ISize) :
a * b * c = a * (b * c)
source
instance instAssociativeInt8HMul :
Std.Associative fun (x1 x2 : Int8) => x1 * x2
source
instance instAssociativeInt16HMul :
Std.Associative fun (x1 x2 : Int16) => x1 * x2
source
instance instAssociativeInt32HMul :
Std.Associative fun (x1 x2 : Int32) => x1 * x2
source
instance instAssociativeInt64HMul :
Std.Associative fun (x1 x2 : Int64) => x1 * x2
source
instance instAssociativeISizeHMul :
Std.Associative fun (x1 x2 : ISize) => x1 * x2
source
@[simp]
theorem Int8.mul_one (a : Int8) :
a * 1 = a
source
@[simp]
theorem Int16.mul_one (a : Int16) :
a * 1 = a
source
@[simp]
theorem Int32.mul_one (a : Int32) :
a * 1 = a
source
@[simp]
theorem Int64.mul_one (a : Int64) :
a * 1 = a
source
@[simp]
theorem ISize.mul_one (a : ISize) :
a * 1 = a
source
@[simp]
theorem Int8.one_mul (a : Int8) :
1 * a = a
source
@[simp]
theorem Int16.one_mul (a : Int16) :
1 * a = a
source
@[simp]
theorem Int32.one_mul (a : Int32) :
1 * a = a
source
@[simp]
theorem Int64.one_mul (a : Int64) :
1 * a = a
source
@[simp]
theorem ISize.one_mul (a : ISize) :
1 * a = a
source
instance instLawfulCommIdentityInt8HMulOfNat :
Std.LawfulCommIdentity (fun (x1 x2 : Int8) => x1 * x2) 1
source
instance instLawfulCommIdentityInt16HMulOfNat :
Std.LawfulCommIdentity (fun (x1 x2 : Int16) => x1 * x2) 1
source
instance instLawfulCommIdentityInt32HMulOfNat :
Std.LawfulCommIdentity (fun (x1 x2 : Int32) => x1 * x2) 1
source
instance instLawfulCommIdentityInt64HMulOfNat :
Std.LawfulCommIdentity (fun (x1 x2 : Int64) => x1 * x2) 1
source
instance instLawfulCommIdentityISizeHMulOfNat :
Std.LawfulCommIdentity (fun (x1 x2 : ISize) => x1 * x2) 1
source
@[simp]
theorem Int8.mul_zero {a : Int8} :
a * 0 = 0
source
@[simp]
theorem Int16.mul_zero {a : Int16} :
a * 0 = 0
source
@[simp]
theorem Int32.mul_zero {a : Int32} :
a * 0 = 0
source
@[simp]
theorem Int64.mul_zero {a : Int64} :
a * 0 = 0
source
@[simp]
theorem ISize.mul_zero {a : ISize} :
a * 0 = 0
source
@[simp]
theorem Int8.zero_mul {a : Int8} :
0 * a = 0
source
@[simp]
theorem Int16.zero_mul {a : Int16} :
0 * a = 0
source
@[simp]
theorem Int32.zero_mul {a : Int32} :
0 * a = 0
source
@[simp]
theorem Int64.zero_mul {a : Int64} :
0 * a = 0
source
@[simp]
theorem ISize.zero_mul {a : ISize} :
0 * a = 0
source
@[simp]
theorem Int8.pow_zero (x : Int8) :
x ^ 0 = 1
source
theorem Int8.pow_succ (x : Int8) (n : Nat) :
x ^ (n + 1) = x ^ n * x
source
@[simp]
theorem Int16.pow_zero (x : Int16) :
x ^ 0 = 1
source
theorem Int16.pow_succ (x : Int16) (n : Nat) :
x ^ (n + 1) = x ^ n * x
source
@[simp]
theorem Int32.pow_zero (x : Int32) :
x ^ 0 = 1
source
theorem Int32.pow_succ (x : Int32) (n : Nat) :
x ^ (n + 1) = x ^ n * x
source
@[simp]
theorem Int64.pow_zero (x : Int64) :
x ^ 0 = 1
source
theorem Int64.pow_succ (x : Int64) (n : Nat) :
x ^ (n + 1) = x ^ n * x
source
@[simp]
theorem ISize.pow_zero (x : ISize) :
x ^ 0 = 1
source
theorem ISize.pow_succ (x : ISize) (n : Nat) :
x ^ (n + 1) = x ^ n * x
source
theorem Int8.mul_add {a b c : Int8} :
a * (b + c) = a * b + a * c
source
theorem Int16.mul_add {a b c : Int16} :
a * (b + c) = a * b + a * c
source
theorem Int32.mul_add {a b c : Int32} :
a * (b + c) = a * b + a * c
source
theorem Int64.mul_add {a b c : Int64} :
a * (b + c) = a * b + a * c
source
theorem ISize.mul_add {a b c : ISize} :
a * (b + c) = a * b + a * c
source
theorem Int8.add_mul {a b c : Int8} :
(a + b) * c = a * c + b * c
source
theorem Int16.add_mul {a b c : Int16} :
(a + b) * c = a * c + b * c
source
theorem Int32.add_mul {a b c : Int32} :
(a + b) * c = a * c + b * c
source
theorem Int64.add_mul {a b c : Int64} :
(a + b) * c = a * c + b * c
source
theorem ISize.add_mul {a b c : ISize} :
(a + b) * c = a * c + b * c
source
theorem Int8.mul_succ {a b : Int8} :
a * (b + 1) = a * b + a
source
theorem Int16.mul_succ {a b : Int16} :
a * (b + 1) = a * b + a
source
theorem Int32.mul_succ {a b : Int32} :
a * (b + 1) = a * b + a
source
theorem Int64.mul_succ {a b : Int64} :
a * (b + 1) = a * b + a
source
theorem ISize.mul_succ {a b : ISize} :
a * (b + 1) = a * b + a
source
theorem Int8.succ_mul {a b : Int8} :
(a + 1) * b = a * b + b
source
theorem Int16.succ_mul {a b : Int16} :
(a + 1) * b = a * b + b
source
theorem Int32.succ_mul {a b : Int32} :
(a + 1) * b = a * b + b
source
theorem Int64.succ_mul {a b : Int64} :
(a + 1) * b = a * b + b
source
theorem ISize.succ_mul {a b : ISize} :
(a + 1) * b = a * b + b
source
theorem Int8.two_mul {a : Int8} :
2 * a = a + a
source
theorem Int16.two_mul {a : Int16} :
2 * a = a + a
source
theorem Int32.two_mul {a : Int32} :
2 * a = a + a
source
theorem Int64.two_mul {a : Int64} :
2 * a = a + a
source
theorem ISize.two_mul {a : ISize} :
2 * a = a + a
source
theorem Int8.mul_two {a : Int8} :
a * 2 = a + a
source
theorem Int16.mul_two {a : Int16} :
a * 2 = a + a
source
theorem Int32.mul_two {a : Int32} :
a * 2 = a + a
source
theorem Int64.mul_two {a : Int64} :
a * 2 = a + a
source
theorem ISize.mul_two {a : ISize} :
a * 2 = a + a
source
theorem Int8.neg_mul (a b : Int8) :
-a * b = -(a * b)
source
theorem Int16.neg_mul (a b : Int16) :
-a * b = -(a * b)
source
theorem Int32.neg_mul (a b : Int32) :
-a * b = -(a * b)
source
theorem Int64.neg_mul (a b : Int64) :
-a * b = -(a * b)
source
theorem ISize.neg_mul (a b : ISize) :
-a * b = -(a * b)
source
theorem Int8.mul_neg (a b : Int8) :
a * -b = -(a * b)
source
theorem Int16.mul_neg (a b : Int16) :
a * -b = -(a * b)
source
theorem Int32.mul_neg (a b : Int32) :
a * -b = -(a * b)
source
theorem Int64.mul_neg (a b : Int64) :
a * -b = -(a * b)
source
theorem ISize.mul_neg (a b : ISize) :
a * -b = -(a * b)
source
theorem Int8.neg_mul_neg (a b : Int8) :
-a * -b = a * b
source
theorem Int16.neg_mul_neg (a b : Int16) :
-a * -b = a * b
source
theorem Int32.neg_mul_neg (a b : Int32) :
-a * -b = a * b
source
theorem Int64.neg_mul_neg (a b : Int64) :
-a * -b = a * b
source
theorem ISize.neg_mul_neg (a b : ISize) :
-a * -b = a * b
source
theorem Int8.neg_mul_comm (a b : Int8) :
-a * b = a * -b
source
theorem Int16.neg_mul_comm (a b : Int16) :
-a * b = a * -b
source
theorem Int32.neg_mul_comm (a b : Int32) :
-a * b = a * -b
source
theorem Int64.neg_mul_comm (a b : Int64) :
-a * b = a * -b
source
theorem ISize.neg_mul_comm (a b : ISize) :
-a * b = a * -b
source
theorem Int8.mul_sub {a b c : Int8} :
a * (b - c) = a * b - a * c
source
theorem Int16.mul_sub {a b c : Int16} :
a * (b - c) = a * b - a * c
source
theorem Int32.mul_sub {a b c : Int32} :
a * (b - c) = a * b - a * c
source
theorem Int64.mul_sub {a b c : Int64} :
a * (b - c) = a * b - a * c
source
theorem ISize.mul_sub {a b c : ISize} :
a * (b - c) = a * b - a * c
source
theorem Int8.sub_mul {a b c : Int8} :
(a - b) * c = a * c - b * c
source
theorem Int16.sub_mul {a b c : Int16} :
(a - b) * c = a * c - b * c
source
theorem Int32.sub_mul {a b c : Int32} :
(a - b) * c = a * c - b * c
source
theorem Int64.sub_mul {a b c : Int64} :
(a - b) * c = a * c - b * c
source
theorem ISize.sub_mul {a b c : ISize} :
(a - b) * c = a * c - b * c
source
theorem Int8.neg_add_mul_eq_mul_not {a b : Int8} :
-(a + a * b) = a * ~~~b
source
theorem Int16.neg_add_mul_eq_mul_not {a b : Int16} :
-(a + a * b) = a * ~~~b
source
theorem Int32.neg_add_mul_eq_mul_not {a b : Int32} :
-(a + a * b) = a * ~~~b
source
theorem Int64.neg_add_mul_eq_mul_not {a b : Int64} :
-(a + a * b) = a * ~~~b
source
theorem ISize.neg_add_mul_eq_mul_not {a b : ISize} :
-(a + a * b) = a * ~~~b
source
theorem Int8.neg_mul_not_eq_add_mul {a b : Int8} :
-(a * ~~~b) = a + a * b
source
theorem Int16.neg_mul_not_eq_add_mul {a b : Int16} :
-(a * ~~~b) = a + a * b
source
theorem Int32.neg_mul_not_eq_add_mul {a b : Int32} :
-(a * ~~~b) = a + a * b
source
theorem Int64.neg_mul_not_eq_add_mul {a b : Int64} :
-(a * ~~~b) = a + a * b
source
theorem ISize.neg_mul_not_eq_add_mul {a b : ISize} :
-(a * ~~~b) = a + a * b
source
theorem Int8.le_of_lt {a b : Int8} :
a < b → a ≤ b
source
theorem Int16.le_of_lt {a b : Int16} :
a < b → a ≤ b
source
theorem Int32.le_of_lt {a b : Int32} :
a < b → a ≤ b
source
theorem Int64.le_of_lt {a b : Int64} :
a < b → a ≤ b
source
theorem ISize.le_of_lt {a b : ISize} :
a < b → a ≤ b
source
theorem Int8.lt_of_le_of_ne {a b : Int8} :
a ≤ b → a ≠ b → a < b
source
theorem Int16.lt_of_le_of_ne {a b : Int16} :
a ≤ b → a ≠ b → a < b
source
theorem Int32.lt_of_le_of_ne {a b : Int32} :
a ≤ b → a ≠ b → a < b
source
theorem Int64.lt_of_le_of_ne {a b : Int64} :
a ≤ b → a ≠ b → a < b
source
theorem ISize.lt_of_le_of_ne {a b : ISize} :
a ≤ b → a ≠ b → a < b
source
theorem Int8.lt_iff_le_and_ne {a b : Int8} :
a < b ↔ a ≤ b ∧ a ≠ b
source
theorem Int16.lt_iff_le_and_ne {a b : Int16} :
a < b ↔ a ≤ b ∧ a ≠ b
source
theorem Int32.lt_iff_le_and_ne {a b : Int32} :
a < b ↔ a ≤ b ∧ a ≠ b
source
theorem Int64.lt_iff_le_and_ne {a b : Int64} :
a < b ↔ a ≤ b ∧ a ≠ b
source
theorem ISize.lt_iff_le_and_ne {a b : ISize} :
a < b ↔ a ≤ b ∧ a ≠ b
source
@[simp]
theorem Int8.lt_irrefl {a : Int8} :
¬a < a
source
@[simp]
theorem Int16.lt_irrefl {a : Int16} :
¬a < a
source
@[simp]
theorem Int32.lt_irrefl {a : Int32} :
¬a < a
source
@[simp]
theorem Int64.lt_irrefl {a : Int64} :
¬a < a
source
@[simp]
theorem ISize.lt_irrefl {a : ISize} :
¬a < a
source
theorem Int8.lt_of_le_of_lt {a b c : Int8} :
a ≤ b → b < c → a < c
source
theorem Int16.lt_of_le_of_lt {a b c : Int16} :
a ≤ b → b < c → a < c
source
theorem Int32.lt_of_le_of_lt {a b c : Int32} :
a ≤ b → b < c → a < c
source
theorem Int64.lt_of_le_of_lt {a b c : Int64} :
a ≤ b → b < c → a < c
source
theorem ISize.lt_of_le_of_lt {a b c : ISize} :
a ≤ b → b < c → a < c
source
theorem Int8.lt_of_lt_of_le {a b c : Int8} :
a < b → b ≤ c → a < c
source
theorem Int16.lt_of_lt_of_le {a b c : Int16} :
a < b → b ≤ c → a < c
source
theorem Int32.lt_of_lt_of_le {a b c : Int32} :
a < b → b ≤ c → a < c
source
theorem Int64.lt_of_lt_of_le {a b c : Int64} :
a < b → b ≤ c → a < c
source
theorem ISize.lt_of_lt_of_le {a b c : ISize} :
a < b → b ≤ c → a < c
source
@[simp]
theorem Int8.minValue_le (a : Int8) :
minValue ≤ a
source
@[simp]
theorem Int16.minValue_le (a : Int16) :
minValue ≤ a
source
@[simp]
theorem Int32.minValue_le (a : Int32) :
minValue ≤ a
source
@[simp]
theorem Int64.minValue_le (a : Int64) :
minValue ≤ a
source
@[simp]
theorem ISize.minValue_le (a : ISize) :
minValue ≤ a
source
@[simp]
theorem Int8.le_maxValue (a : Int8) :
a ≤ maxValue
source
@[simp]
theorem Int16.le_maxValue (a : Int16) :
a ≤ maxValue
source
@[simp]
theorem Int32.le_maxValue (a : Int32) :
a ≤ maxValue
source
@[simp]
theorem Int64.le_maxValue (a : Int64) :
a ≤ maxValue
source
@[simp]
theorem ISize.le_maxValue (a : ISize) :
a ≤ maxValue
source
@[simp]
theorem Int8.not_lt_minValue {a : Int8} :
¬a < minValue
source
@[simp]
theorem Int16.not_lt_minValue {a : Int16} :
¬a < minValue
source
@[simp]
theorem Int32.not_lt_minValue {a : Int32} :
¬a < minValue
source
@[simp]
theorem Int64.not_lt_minValue {a : Int64} :
¬a < minValue
source
@[simp]
theorem ISize.not_lt_minValue {a : ISize} :
¬a < minValue
source
@[simp]
theorem Int8.not_maxValue_lt {a : Int8} :
¬maxValue < a
source
@[simp]
theorem Int16.not_maxValue_lt {a : Int16} :
¬maxValue < a
source
@[simp]
theorem Int32.not_maxValue_lt {a : Int32} :
¬maxValue < a
source
@[simp]
theorem Int64.not_maxValue_lt {a : Int64} :
¬maxValue < a
source
@[simp]
theorem ISize.not_maxValue_lt {a : ISize} :
¬maxValue < a
source
@[simp]
theorem Int8.le_refl (a : Int8) :
a ≤ a
source
@[simp]
theorem Int16.le_refl (a : Int16) :
a ≤ a
source
@[simp]
theorem Int32.le_refl (a : Int32) :
a ≤ a
source
@[simp]
theorem Int64.le_refl (a : Int64) :
a ≤ a
source
@[simp]
theorem ISize.le_refl (a : ISize) :
a ≤ a
source
theorem Int8.le_rfl {a : Int8} :
a ≤ a
source
theorem Int16.le_rfl {a : Int16} :
a ≤ a
source
theorem Int32.le_rfl {a : Int32} :
a ≤ a
source
theorem Int64.le_rfl {a : Int64} :
a ≤ a
source
theorem ISize.le_rfl {a : ISize} :
a ≤ a
source
theorem Int8.le_antisymm_iff {a b : Int8} :
a = b ↔ a ≤ b ∧ b ≤ a
source
theorem Int16.le_antisymm_iff {a b : Int16} :
a = b ↔ a ≤ b ∧ b ≤ a
source
theorem Int32.le_antisymm_iff {a b : Int32} :
a = b ↔ a ≤ b ∧ b ≤ a
source
theorem Int64.le_antisymm_iff {a b : Int64} :
a = b ↔ a ≤ b ∧ b ≤ a
source
theorem ISize.le_antisymm_iff {a b : ISize} :
a = b ↔ a ≤ b ∧ b ≤ a
source
theorem Int8.le_antisymm {a b : Int8} :
a ≤ b → b ≤ a → a = b
source
theorem Int16.le_antisymm {a b : Int16} :
a ≤ b → b ≤ a → a = b
source
theorem Int32.le_antisymm {a b : Int32} :
a ≤ b → b ≤ a → a = b
source
theorem Int64.le_antisymm {a b : Int64} :
a ≤ b → b ≤ a → a = b
source
theorem ISize.le_antisymm {a b : ISize} :
a ≤ b → b ≤ a → a = b
source
@[simp]
theorem Int8.le_minValue_iff {a : Int8} :
a ≤ minValue ↔ a = minValue
source
@[simp]
theorem Int16.le_minValue_iff {a : Int16} :
a ≤ minValue ↔ a = minValue
source
@[simp]
theorem Int32.le_minValue_iff {a : Int32} :
a ≤ minValue ↔ a = minValue
source
@[simp]
theorem Int64.le_minValue_iff {a : Int64} :
a ≤ minValue ↔ a = minValue
source
@[simp]
theorem ISize.le_minValue_iff {a : ISize} :
a ≤ minValue ↔ a = minValue
source
@[simp]
theorem Int8.maxValue_le_iff {a : Int8} :
maxValue ≤ a ↔ a = maxValue
source
@[simp]
theorem Int16.maxValue_le_iff {a : Int16} :
maxValue ≤ a ↔ a = maxValue
source
@[simp]
theorem Int32.maxValue_le_iff {a : Int32} :
maxValue ≤ a ↔ a = maxValue
source
@[simp]
theorem Int64.maxValue_le_iff {a : Int64} :
maxValue ≤ a ↔ a = maxValue
source
@[simp]
theorem ISize.maxValue_le_iff {a : ISize} :
maxValue ≤ a ↔ a = maxValue
source
@[simp]
theorem Int8.zero_div {a : Int8} :
0 / a = 0
source
@[simp]
theorem Int16.zero_div {a : Int16} :
0 / a = 0
source
@[simp]
theorem Int32.zero_div {a : Int32} :
0 / a = 0
source
@[simp]
theorem Int64.zero_div {a : Int64} :
0 / a = 0
source
@[simp]
theorem ISize.zero_div {a : ISize} :
0 / a = 0
source
@[simp]
theorem Int8.div_zero {a : Int8} :
a / 0 = 0
source
@[simp]
theorem Int16.div_zero {a : Int16} :
a / 0 = 0
source
@[simp]
theorem Int32.div_zero {a : Int32} :
a / 0 = 0
source
@[simp]
theorem Int64.div_zero {a : Int64} :
a / 0 = 0
source
@[simp]
theorem ISize.div_zero {a : ISize} :
a / 0 = 0
source
@[simp]
theorem Int8.div_one {a : Int8} :
a / 1 = a
source
@[simp]
theorem Int16.div_one {a : Int16} :
a / 1 = a
source
@[simp]
theorem Int32.div_one {a : Int32} :
a / 1 = a
source
@[simp]
theorem Int64.div_one {a : Int64} :
a / 1 = a
source
@[simp]
theorem ISize.div_one {a : ISize} :
a / 1 = a
source
theorem Int8.div_self {a : Int8} :
a / a = if a = 0 then 0 else 1
source
theorem Int16.div_self {a : Int16} :
a / a = if a = 0 then 0 else 1
source
theorem Int32.div_self {a : Int32} :
a / a = if a = 0 then 0 else 1
source
theorem Int64.div_self {a : Int64} :
a / a = if a = 0 then 0 else 1
source
theorem ISize.div_self {a : ISize} :
a / a = if a = 0 then 0 else 1
source
@[simp]
theorem Int8.mod_zero {a : Int8} :
a % 0 = a
source
@[simp]
theorem Int16.mod_zero {a : Int16} :
a % 0 = a
source
@[simp]
theorem Int32.mod_zero {a : Int32} :
a % 0 = a
source
@[simp]
theorem Int64.mod_zero {a : Int64} :
a % 0 = a
source
@[simp]
theorem ISize.mod_zero {a : ISize} :
a % 0 = a
source
@[simp]
theorem Int8.zero_mod {a : Int8} :
0 % a = 0
source
@[simp]
theorem Int16.zero_mod {a : Int16} :
0 % a = 0
source
@[simp]
theorem Int32.zero_mod {a : Int32} :
0 % a = 0
source
@[simp]
theorem Int64.zero_mod {a : Int64} :
0 % a = 0
source
@[simp]
theorem ISize.zero_mod {a : ISize} :
0 % a = 0
source
@[simp]
theorem Int8.mod_one {a : Int8} :
a % 1 = 0
source
@[simp]
theorem Int16.mod_one {a : Int16} :
a % 1 = 0
source
@[simp]
theorem Int32.mod_one {a : Int32} :
a % 1 = 0
source
@[simp]
theorem Int64.mod_one {a : Int64} :
a % 1 = 0
source
@[simp]
theorem ISize.mod_one {a : ISize} :
a % 1 = 0
source
@[simp]
theorem Int8.mod_self {a : Int8} :
a % a = 0
source
@[simp]
theorem Int16.mod_self {a : Int16} :
a % a = 0
source
@[simp]
theorem Int32.mod_self {a : Int32} :
a % a = 0
source
@[simp]
theorem Int64.mod_self {a : Int64} :
a % a = 0
source
@[simp]
theorem ISize.mod_self {a : ISize} :
a % a = 0
source
@[simp]
theorem Int8.not_lt {a b : Int8} :
¬a < b ↔ b ≤ a
source
@[simp]
theorem Int16.not_lt {a b : Int16} :
¬a < b ↔ b ≤ a
source
@[simp]
theorem Int32.not_lt {a b : Int32} :
¬a < b ↔ b ≤ a
source
@[simp]
theorem Int64.not_lt {a b : Int64} :
¬a < b ↔ b ≤ a
source
@[simp]
theorem ISize.not_lt {a b : ISize} :
¬a < b ↔ b ≤ a
source
theorem Int8.le_trans {a b c : Int8} :
a ≤ b → b ≤ c → a ≤ c
source
theorem Int16.le_trans {a b c : Int16} :
a ≤ b → b ≤ c → a ≤ c
source
theorem Int32.le_trans {a b c : Int32} :
a ≤ b → b ≤ c → a ≤ c
source
theorem Int64.le_trans {a b c : Int64} :
a ≤ b → b ≤ c → a ≤ c
source
theorem ISize.le_trans {a b c : ISize} :
a ≤ b → b ≤ c → a ≤ c
source
theorem Int8.lt_trans {a b c : Int8} :
a < b → b < c → a < c
source
theorem Int16.lt_trans {a b c : Int16} :
a < b → b < c → a < c
source
theorem Int32.lt_trans {a b c : Int32} :
a < b → b < c → a < c
source
theorem Int64.lt_trans {a b c : Int64} :
a < b → b < c → a < c
source
theorem ISize.lt_trans {a b c : ISize} :
a < b → b < c → a < c
source
theorem Int8.le_total (a b : Int8) :
a ≤ b ∨ b ≤ a
source
theorem Int16.le_total (a b : Int16) :
a ≤ b ∨ b ≤ a
source
theorem Int32.le_total (a b : Int32) :
a ≤ b ∨ b ≤ a
source
theorem Int64.le_total (a b : Int64) :
a ≤ b ∨ b ≤ a
source
theorem ISize.le_total (a b : ISize) :
a ≤ b ∨ b ≤ a
source
theorem Int8.lt_asymm {a b : Int8} :
a < b → ¬b < a
source
theorem Int16.lt_asymm {a b : Int16} :
a < b → ¬b < a
source
theorem Int32.lt_asymm {a b : Int32} :
a < b → ¬b < a
source
theorem Int64.lt_asymm {a b : Int64} :
a < b → ¬b < a
source
theorem ISize.lt_asymm {a b : ISize} :
a < b → ¬b < a
source
instance Int8.instIsLinearOrder :
Std.IsLinearOrder Int8
source
instance instLawfulOrderLTInt8 :
Std.LawfulOrderLT Int8
source
instance Int16.instIsLinearOrder :
Std.IsLinearOrder Int16
source
instance instLawfulOrderLTInt16 :
Std.LawfulOrderLT Int16
source
instance Int32.instIsLinearOrder :
Std.IsLinearOrder Int32
source
instance instLawfulOrderLTInt32 :
Std.LawfulOrderLT Int32
source
instance Int64.instIsLinearOrder :
Std.IsLinearOrder Int64
source
instance instLawfulOrderLTInt64 :
Std.LawfulOrderLT Int64
source
instance ISize.instIsLinearOrder :
Std.IsLinearOrder ISize
source
instance instLawfulOrderLTISize :
Std.LawfulOrderLT ISize
source
theorem Int8.add_neg_eq_sub {a b : Int8} :
a + -b = a - b
source
theorem Int16.add_neg_eq_sub {a b : Int16} :
a + -b = a - b
source
theorem Int32.add_neg_eq_sub {a b : Int32} :
a + -b = a - b
source
theorem Int64.add_neg_eq_sub {a b : Int64} :
a + -b = a - b
source
theorem ISize.add_neg_eq_sub {a b : ISize} :
a + -b = a - b
source
theorem Int8.neg_eq_neg_one_mul (a : Int8) :
-a = -1 * a
source
theorem Int16.neg_eq_neg_one_mul (a : Int16) :
-a = -1 * a
source
theorem Int32.neg_eq_neg_one_mul (a : Int32) :
-a = -1 * a
source
theorem Int64.neg_eq_neg_one_mul (a : Int64) :
-a = -1 * a
source
theorem ISize.neg_eq_neg_one_mul (a : ISize) :
-a = -1 * a
source
@[simp]
theorem Int8.add_sub_cancel (a b : Int8) :
a + b - b = a
source
@[simp]
theorem Int16.add_sub_cancel (a b : Int16) :
a + b - b = a
source
@[simp]
theorem Int32.add_sub_cancel (a b : Int32) :
a + b - b = a
source
@[simp]
theorem Int64.add_sub_cancel (a b : Int64) :
a + b - b = a
source
@[simp]
theorem ISize.add_sub_cancel (a b : ISize) :
a + b - b = a
source
theorem Int8.lt_or_lt_of_ne {a b : Int8} :
a ≠ b → a < b ∨ b < a
source
theorem Int16.lt_or_lt_of_ne {a b : Int16} :
a ≠ b → a < b ∨ b < a
source
theorem Int32.lt_or_lt_of_ne {a b : Int32} :
a ≠ b → a < b ∨ b < a
source
theorem Int64.lt_or_lt_of_ne {a b : Int64} :
a ≠ b → a < b ∨ b < a
source
theorem ISize.lt_or_lt_of_ne {a b : ISize} :
a ≠ b → a < b ∨ b < a
source
theorem Int8.lt_or_le (a b : Int8) :
a < b ∨ b ≤ a
source
theorem Int16.lt_or_le (a b : Int16) :
a < b ∨ b ≤ a
source
theorem Int32.lt_or_le (a b : Int32) :
a < b ∨ b ≤ a
source
theorem Int64.lt_or_le (a b : Int64) :
a < b ∨ b ≤ a
source
theorem ISize.lt_or_le (a b : ISize) :
a < b ∨ b ≤ a
source
theorem Int8.le_or_lt (a b : Int8) :
a ≤ b ∨ b < a
source
theorem Int16.le_or_lt (a b : Int16) :
a ≤ b ∨ b < a
source
theorem Int32.le_or_lt (a b : Int32) :
a ≤ b ∨ b < a
source
theorem Int64.le_or_lt (a b : Int64) :
a ≤ b ∨ b < a
source
theorem ISize.le_or_lt (a b : ISize) :
a ≤ b ∨ b < a
source
theorem Int8.le_of_eq {a b : Int8} :
a = b → a ≤ b
source
theorem Int16.le_of_eq {a b : Int16} :
a = b → a ≤ b
source
theorem Int32.le_of_eq {a b : Int32} :
a = b → a ≤ b
source
theorem Int64.le_of_eq {a b : Int64} :
a = b → a ≤ b
source
theorem ISize.le_of_eq {a b : ISize} :
a = b → a ≤ b
source
theorem Int8.le_iff_lt_or_eq {a b : Int8} :
a ≤ b ↔ a < b ∨ a = b
source
theorem Int16.le_iff_lt_or_eq {a b : Int16} :
a ≤ b ↔ a < b ∨ a = b
source
theorem Int32.le_iff_lt_or_eq {a b : Int32} :
a ≤ b ↔ a < b ∨ a = b
source
theorem Int64.le_iff_lt_or_eq {a b : Int64} :
a ≤ b ↔ a < b ∨ a = b
source
theorem ISize.le_iff_lt_or_eq {a b : ISize} :
a ≤ b ↔ a < b ∨ a = b
source
theorem Int8.lt_or_eq_of_le {a b : Int8} :
a ≤ b → a < b ∨ a = b
source
theorem Int16.lt_or_eq_of_le {a b : Int16} :
a ≤ b → a < b ∨ a = b
source
theorem Int32.lt_or_eq_of_le {a b : Int32} :
a ≤ b → a < b ∨ a = b
source
theorem Int64.lt_or_eq_of_le {a b : Int64} :
a ≤ b → a < b ∨ a = b
source
theorem ISize.lt_or_eq_of_le {a b : ISize} :
a ≤ b → a < b ∨ a = b
source
theorem Int8.toInt_eq_toNatClampNeg {a : Int8} (ha : 0 ≤ a) :
a.toInt = ↑a.toNatClampNeg
source
theorem Int16.toInt_eq_toNatClampNeg {a : Int16} (ha : 0 ≤ a) :
a.toInt = ↑a.toNatClampNeg
source
theorem Int32.toInt_eq_toNatClampNeg {a : Int32} (ha : 0 ≤ a) :
a.toInt = ↑a.toNatClampNeg
source
theorem Int64.toInt_eq_toNatClampNeg {a : Int64} (ha : 0 ≤ a) :
a.toInt = ↑a.toNatClampNeg
source
theorem ISize.toInt_eq_toNatClampNeg {a : ISize} (ha : 0 ≤ a) :
a.toInt = ↑a.toNatClampNeg
source
@[simp]
theorem UInt8.toInt8_add (a b : UInt8) :
(a + b).toInt8 = a.toInt8 + b.toInt8
source
@[simp]
theorem UInt16.toInt16_add (a b : UInt16) :
(a + b).toInt16 = a.toInt16 + b.toInt16
source
@[simp]
theorem UInt32.toInt32_add (a b : UInt32) :
(a + b).toInt32 = a.toInt32 + b.toInt32
source
@[simp]
theorem UInt64.toInt64_add (a b : UInt64) :
(a + b).toInt64 = a.toInt64 + b.toInt64
source
@[simp]
theorem USize.toISize_add (a b : USize) :
(a + b).toISize = a.toISize + b.toISize
source
@[simp]
theorem UInt8.toInt8_neg (a : UInt8) :
(-a).toInt8 = -a.toInt8
source
@[simp]
theorem UInt16.toInt16_neg (a : UInt16) :
(-a).toInt16 = -a.toInt16
source
@[simp]
theorem UInt32.toInt32_neg (a : UInt32) :
(-a).toInt32 = -a.toInt32
source
@[simp]
theorem UInt64.toInt64_neg (a : UInt64) :
(-a).toInt64 = -a.toInt64
source
@[simp]
theorem USize.toISize_neg (a : USize) :
(-a).toISize = -a.toISize
source
@[simp]
theorem UInt8.toInt8_sub (a b : UInt8) :
(a - b).toInt8 = a.toInt8 - b.toInt8
source
@[simp]
theorem UInt16.toInt16_sub (a b : UInt16) :
(a - b).toInt16 = a.toInt16 - b.toInt16
source
@[simp]
theorem UInt32.toInt32_sub (a b : UInt32) :
(a - b).toInt32 = a.toInt32 - b.toInt32
source
@[simp]
theorem UInt64.toInt64_sub (a b : UInt64) :
(a - b).toInt64 = a.toInt64 - b.toInt64
source
@[simp]
theorem USize.toISize_sub (a b : USize) :
(a - b).toISize = a.toISize - b.toISize
source
@[simp]
theorem UInt8.toInt8_mul (a b : UInt8) :
(a * b).toInt8 = a.toInt8 * b.toInt8
source
@[simp]
theorem UInt16.toInt16_mul (a b : UInt16) :
(a * b).toInt16 = a.toInt16 * b.toInt16
source
@[simp]
theorem UInt32.toInt32_mul (a b : UInt32) :
(a * b).toInt32 = a.toInt32 * b.toInt32
source
@[simp]
theorem UInt64.toInt64_mul (a b : UInt64) :
(a * b).toInt64 = a.toInt64 * b.toInt64
source
@[simp]
theorem USize.toISize_mul (a b : USize) :
(a * b).toISize = a.toISize * b.toISize
source
@[simp]
theorem Int8.toUInt8_add (a b : Int8) :
(a + b).toUInt8 = a.toUInt8 + b.toUInt8
source
@[simp]
theorem Int16.toUInt16_add (a b : Int16) :
(a + b).toUInt16 = a.toUInt16 + b.toUInt16
source
@[simp]
theorem Int32.toUInt32_add (a b : Int32) :
(a + b).toUInt32 = a.toUInt32 + b.toUInt32
source
@[simp]
theorem Int64.toUInt64_add (a b : Int64) :
(a + b).toUInt64 = a.toUInt64 + b.toUInt64
source
@[simp]
theorem ISize.toUSize_add (a b : ISize) :
(a + b).toUSize = a.toUSize + b.toUSize
source
@[simp]
theorem Int8.toUInt8_neg (a : Int8) :
(-a).toUInt8 = -a.toUInt8
source
@[simp]
theorem Int16.toUInt16_neg (a : Int16) :
(-a).toUInt16 = -a.toUInt16
source
@[simp]
theorem Int32.toUInt32_neg (a : Int32) :
(-a).toUInt32 = -a.toUInt32
source
@[simp]
theorem Int64.toUInt64_neg (a : Int64) :
(-a).toUInt64 = -a.toUInt64
source
@[simp]
theorem ISize.toUSize_neg (a : ISize) :
(-a).toUSize = -a.toUSize
source
@[simp]
theorem Int8.toUInt8_sub (a b : Int8) :
(a - b).toUInt8 = a.toUInt8 - b.toUInt8
source
@[simp]
theorem Int16.toUInt16_sub (a b : Int16) :
(a - b).toUInt16 = a.toUInt16 - b.toUInt16
source
@[simp]
theorem Int32.toUInt32_sub (a b : Int32) :
(a - b).toUInt32 = a.toUInt32 - b.toUInt32
source
@[simp]
theorem Int64.toUInt64_sub (a b : Int64) :
(a - b).toUInt64 = a.toUInt64 - b.toUInt64
source
@[simp]
theorem ISize.toUSize_sub (a b : ISize) :
(a - b).toUSize = a.toUSize - b.toUSize
source
@[simp]
theorem Int8.toUInt8_mul (a b : Int8) :
(a * b).toUInt8 = a.toUInt8 * b.toUInt8
source
@[simp]
theorem Int16.toUInt16_mul (a b : Int16) :
(a * b).toUInt16 = a.toUInt16 * b.toUInt16
source
@[simp]
theorem Int32.toUInt32_mul (a b : Int32) :
(a * b).toUInt32 = a.toUInt32 * b.toUInt32
source
@[simp]
theorem Int64.toUInt64_mul (a b : Int64) :
(a * b).toUInt64 = a.toUInt64 * b.toUInt64
source
@[simp]
theorem ISize.toUSize_mul (a b : ISize) :
(a * b).toUSize = a.toUSize * b.toUSize
source
theorem Int8.toNatClampNeg_le {a b : Int8} (hab : a ≤ b) :
a.toNatClampNeg ≤ b.toNatClampNeg
source
theorem Int16.toNatClampNeg_le {a b : Int16} (hab : a ≤ b) :
a.toNatClampNeg ≤ b.toNatClampNeg
source
theorem Int32.toNatClampNeg_le {a b : Int32} (hab : a ≤ b) :
a.toNatClampNeg ≤ b.toNatClampNeg
source
theorem Int64.toNatClampNeg_le {a b : Int64} (hab : a ≤ b) :
a.toNatClampNeg ≤ b.toNatClampNeg
source
theorem ISize.toNatClampNeg_le {a b : ISize} (hab : a ≤ b) :
a.toNatClampNeg ≤ b.toNatClampNeg
source
theorem Int8.toUInt8_le {a b : Int8} (ha : 0 ≤ a) (hab : a ≤ b) :
a.toUInt8 ≤ b.toUInt8
source
theorem Int16.toUInt16_le {a b : Int16} (ha : 0 ≤ a) (hab : a ≤ b) :
a.toUInt16 ≤ b.toUInt16
source
theorem Int32.toUInt32_le {a b : Int32} (ha : 0 ≤ a) (hab : a ≤ b) :
a.toUInt32 ≤ b.toUInt32
source
theorem Int64.toUInt64_le {a b : Int64} (ha : 0 ≤ a) (hab : a ≤ b) :
a.toUInt64 ≤ b.toUInt64
source
theorem ISize.toUSize_le {a b : ISize} (ha : 0 ≤ a) (hab : a ≤ b) :
a.toUSize ≤ b.toUSize
source
theorem Int8.zero_le_ofNat_of_lt {a : Nat} (ha : a < 2 ^ 7) :
0 ≤ ofNat a
source
theorem Int16.zero_le_ofNat_of_lt {a : Nat} (ha : a < 2 ^ 15) :
0 ≤ ofNat a
source
theorem Int32.zero_le_ofNat_of_lt {a : Nat} (ha : a < 2 ^ 31) :
0 ≤ ofNat a
source
theorem Int64.zero_le_ofNat_of_lt {a : Nat} (ha : a < 2 ^ 63) :
0 ≤ ofNat a
source
theorem ISize.zero_le_ofNat_of_lt {a : Nat} (ha : a < 2 ^ (System.Platform.numBits - 1)) :
0 ≤ ofNat a
source
theorem Int8.sub_nonneg_of_le {a b : Int8} (hb : 0 ≤ b) (hab : b ≤ a) :
0 ≤ a - b
source
theorem Int16.sub_nonneg_of_le {a b : Int16} (hb : 0 ≤ b) (hab : b ≤ a) :
0 ≤ a - b
source
theorem Int32.sub_nonneg_of_le {a b : Int32} (hb : 0 ≤ b) (hab : b ≤ a) :
0 ≤ a - b
source
theorem Int64.sub_nonneg_of_le {a b : Int64} (hb : 0 ≤ b) (hab : b ≤ a) :
0 ≤ a - b
source
theorem ISize.sub_nonneg_of_le {a b : ISize} (hb : 0 ≤ b) (hab : b ≤ a) :
0 ≤ a - b
source
theorem Int8.toNatClampNeg_sub_of_le {a b : Int8} (hb : 0 ≤ b) (hab : b ≤ a) :
(a - b).toNatClampNeg = a.toNatClampNeg - b.toNatClampNeg
source
theorem Int16.toNatClampNeg_sub_of_le {a b : Int16} (hb : 0 ≤ b) (hab : b ≤ a) :
(a - b).toNatClampNeg = a.toNatClampNeg - b.toNatClampNeg
source
theorem Int32.toNatClampNeg_sub_of_le {a b : Int32} (hb : 0 ≤ b) (hab : b ≤ a) :
(a - b).toNatClampNeg = a.toNatClampNeg - b.toNatClampNeg
source
theorem Int64.toNatClampNeg_sub_of_le {a b : Int64} (hb : 0 ≤ b) (hab : b ≤ a) :
(a - b).toNatClampNeg = a.toNatClampNeg - b.toNatClampNeg
source
theorem ISize.toNatClampNeg_sub_of_le {a b : ISize} (hb : 0 ≤ b) (hab : b ≤ a) :
(a - b).toNatClampNeg = a.toNatClampNeg - b.toNatClampNeg
source
theorem Int8.toInt_sub_of_le (a b : Int8) (hb : 0 ≤ b) (h : b ≤ a) :
(a - b).toInt = a.toInt - b.toInt
source
theorem Int16.toInt_sub_of_le (a b : Int16) (hb : 0 ≤ b) (h : b ≤ a) :
(a - b).toInt = a.toInt - b.toInt
source
theorem Int32.toInt_sub_of_le (a b : Int32) (hb : 0 ≤ b) (h : b ≤ a) :
(a - b).toInt = a.toInt - b.toInt
source
theorem Int64.toInt_sub_of_le (a b : Int64) (hb : 0 ≤ b) (h : b ≤ a) :
(a - b).toInt = a.toInt - b.toInt
source
theorem ISize.toInt_sub_of_le (a b : ISize) (hb : 0 ≤ b) (h : b ≤ a) :
(a - b).toInt = a.toInt - b.toInt
source
theorem Int8.sub_le {a b : Int8} (hb : 0 ≤ b) (hab : b ≤ a) :
a - b ≤ a
source
theorem Int16.sub_le {a b : Int16} (hb : 0 ≤ b) (hab : b ≤ a) :
a - b ≤ a
source
theorem Int32.sub_le {a b : Int32} (hb : 0 ≤ b) (hab : b ≤ a) :
a - b ≤ a
source
theorem Int64.sub_le {a b : Int64} (hb : 0 ≤ b) (hab : b ≤ a) :
a - b ≤ a
source
theorem ISize.sub_le {a b : ISize} (hb : 0 ≤ b) (hab : b ≤ a) :
a - b ≤ a
source
theorem Int8.sub_lt {a b : Int8} (hb : 0 < b) (hab : b ≤ a) :
a - b < a
source
theorem Int16.sub_lt {a b : Int16} (hb : 0 < b) (hab : b ≤ a) :
a - b < a
source
theorem Int32.sub_lt {a b : Int32} (hb : 0 < b) (hab : b ≤ a) :
a - b < a
source
theorem Int64.sub_lt {a b : Int64} (hb : 0 < b) (hab : b ≤ a) :
a - b < a
source
theorem ISize.sub_lt {a b : ISize} (hb : 0 < b) (hab : b ≤ a) :
a - b < a
source
theorem Int8.ne_of_lt {a b : Int8} :
a < b → a ≠ b
source
theorem Int16.ne_of_lt {a b : Int16} :
a < b → a ≠ b
source
theorem Int32.ne_of_lt {a b : Int32} :
a < b → a ≠ b
source
theorem Int64.ne_of_lt {a b : Int64} :
a < b → a ≠ b
source
theorem ISize.ne_of_lt {a b : ISize} :
a < b → a ≠ b
source
@[simp]
theorem Int8.toInt_mod (a b : Int8) :
(a % b).toInt = a.toInt.tmod b.toInt
source
@[simp]
theorem Int16.toInt_mod (a b : Int16) :
(a % b).toInt = a.toInt.tmod b.toInt
source
@[simp]
theorem Int32.toInt_mod (a b : Int32) :
(a % b).toInt = a.toInt.tmod b.toInt
source
@[simp]
theorem Int64.toInt_mod (a b : Int64) :
(a % b).toInt = a.toInt.tmod b.toInt
source
@[simp]
theorem ISize.toInt_mod (a b : ISize) :
(a % b).toInt = a.toInt.tmod b.toInt
source
@[simp]
theorem Int8.toInt16_mod (a b : Int8) :
(a % b).toInt16 = a.toInt16 % b.toInt16
source
@[simp]
theorem Int8.toInt32_mod (a b : Int8) :
(a % b).toInt32 = a.toInt32 % b.toInt32
source
@[simp]
theorem Int8.toInt64_mod (a b : Int8) :
(a % b).toInt64 = a.toInt64 % b.toInt64
source
@[simp]
theorem Int8.toISize_mod (a b : Int8) :
(a % b).toISize = a.toISize % b.toISize
source
@[simp]
theorem Int16.toInt32_mod (a b : Int16) :
(a % b).toInt32 = a.toInt32 % b.toInt32
source
@[simp]
theorem Int16.toInt64_mod (a b : Int16) :
(a % b).toInt64 = a.toInt64 % b.toInt64
source
@[simp]
theorem Int16.toISize_mod (a b : Int16) :
(a % b).toISize = a.toISize % b.toISize
source
@[simp]
theorem Int32.toInt64_mod (a b : Int32) :
(a % b).toInt64 = a.toInt64 % b.toInt64
source
@[simp]
theorem Int32.toISize_mod (a b : Int32) :
(a % b).toISize = a.toISize % b.toISize
source
@[simp]
theorem ISize.toInt64_mod (a b : ISize) :
(a % b).toInt64 = a.toInt64 % b.toInt64
source
theorem Int8.ofInt_tmod {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) :
ofInt (a.tmod b) = ofInt a % ofInt b
source
theorem Int16.ofInt_tmod {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) :
ofInt (a.tmod b) = ofInt a % ofInt b
source
theorem Int32.ofInt_tmod {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) :
ofInt (a.tmod b) = ofInt a % ofInt b
source
theorem Int64.ofInt_tmod {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) :
ofInt (a.tmod b) = ofInt a % ofInt b
source
theorem ISize.ofInt_tmod {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) :
ofInt (a.tmod b) = ofInt a % ofInt b
source
theorem Int8.ofInt_eq_ofIntLE_mod {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) :
ofInt (a.tmod b) = ofIntLE a ha₁ ha₂ % ofIntLE b hb₁ hb₂
source
theorem Int16.ofInt_eq_ofIntLE_mod {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) :
ofInt (a.tmod b) = ofIntLE a ha₁ ha₂ % ofIntLE b hb₁ hb₂
source
theorem Int32.ofInt_eq_ofIntLE_mod {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) :
ofInt (a.tmod b) = ofIntLE a ha₁ ha₂ % ofIntLE b hb₁ hb₂
source
theorem Int64.ofInt_eq_ofIntLE_mod {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) :
ofInt (a.tmod b) = ofIntLE a ha₁ ha₂ % ofIntLE b hb₁ hb₂
source
theorem ISize.ofInt_eq_ofIntLE_mod {a b : Int} (ha₁ : minValue.toInt ≤ a) (ha₂ : a ≤ maxValue.toInt) (hb₁ : minValue.toInt ≤ b) (hb₂ : b ≤ maxValue.toInt) :
ofInt (a.tmod b) = ofIntLE a ha₁ ha₂ % ofIntLE b hb₁ hb₂
source
theorem Int8.ofNat_mod {a b : Nat} (ha : a < 2 ^ 7) (hb : b < 2 ^ 7) :
ofNat (a % b) = ofNat a % ofNat b
source
theorem Int16.ofNat_mod {a b : Nat} (ha : a < 2 ^ 15) (hb : b < 2 ^ 15) :
ofNat (a % b) = ofNat a % ofNat b
source
theorem Int32.ofNat_mod {a b : Nat} (ha : a < 2 ^ 31) (hb : b < 2 ^ 31) :
ofNat (a % b) = ofNat a % ofNat b
source
theorem Int64.ofNat_mod {a b : Nat} (ha : a < 2 ^ 63) (hb : b < 2 ^ 63) :
ofNat (a % b) = ofNat a % ofNat b
source
theorem ISize.ofNat_mod {a b : Nat} (ha : a < 2 ^ (System.Platform.numBits - 1)) (hb : b < 2 ^ (System.Platform.numBits - 1)) :
ofNat (a % b) = ofNat a % ofNat b