Documentation

Init.Data.SInt.Bitwise

source
def commandDeclare_bitwise_int_theorems__ :
Lean.ParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem Int8.toBitVec_and (a b : Int8) :
(a &&& b).toBitVec = a.toBitVec &&& b.toBitVec
source
@[simp]
theorem Int8.toBitVec_xor (a b : Int8) :
(a ^^^ b).toBitVec = a.toBitVec ^^^ b.toBitVec
source
@[simp]
theorem Int8.toBitVec_sub {a b : Int8} :
(a - b).toBitVec = a.toBitVec - b.toBitVec
source
@[simp]
theorem Int8.toBitVec_div {a b : Int8} :
(a / b).toBitVec = a.toBitVec.sdiv b.toBitVec
source
@[simp]
theorem Int8.toBitVec_shiftLeft (a b : Int8) :
(a <<< b).toBitVec = a.toBitVec <<< b.toBitVec.smod 8
source
@[simp]
theorem Int8.toBitVec_mod {a b : Int8} :
(a % b).toBitVec = a.toBitVec.srem b.toBitVec
source
@[simp]
theorem Int8.toBitVec_shiftRight (a b : Int8) :
(a >>> b).toBitVec = a.toBitVec.sshiftRight' (b.toBitVec.smod 8)
source
@[simp]
theorem Int8.toBitVec_mul {a b : Int8} :
(a * b).toBitVec = a.toBitVec * b.toBitVec
source
@[simp]
theorem Int8.toBitVec_or (a b : Int8) :
(a ||| b).toBitVec = a.toBitVec ||| b.toBitVec
source
@[simp]
theorem Int8.toBitVec_abs (a : Int8) :
a.abs.toBitVec = a.toBitVec.abs
source
@[simp]
theorem Int8.toBitVec_add {a b : Int8} :
(a + b).toBitVec = a.toBitVec + b.toBitVec
source
@[simp]
theorem Int8.toBitVec_not {a : Int8} :
(~~~a).toBitVec = ~~~a.toBitVec
source
@[simp]
theorem Int16.toBitVec_div {a b : Int16} :
(a / b).toBitVec = a.toBitVec.sdiv b.toBitVec
source
@[simp]
theorem Int16.toBitVec_xor (a b : Int16) :
(a ^^^ b).toBitVec = a.toBitVec ^^^ b.toBitVec
source
@[simp]
theorem Int16.toBitVec_not {a : Int16} :
(~~~a).toBitVec = ~~~a.toBitVec
source
@[simp]
theorem Int16.toBitVec_mod {a b : Int16} :
(a % b).toBitVec = a.toBitVec.srem b.toBitVec
source
@[simp]
theorem Int16.toBitVec_or (a b : Int16) :
(a ||| b).toBitVec = a.toBitVec ||| b.toBitVec
source
@[simp]
theorem Int16.toBitVec_shiftLeft (a b : Int16) :
(a <<< b).toBitVec = a.toBitVec <<< b.toBitVec.smod 16
source
@[simp]
theorem Int16.toBitVec_add {a b : Int16} :
(a + b).toBitVec = a.toBitVec + b.toBitVec
source
@[simp]
theorem Int16.toBitVec_shiftRight (a b : Int16) :
(a >>> b).toBitVec = a.toBitVec.sshiftRight' (b.toBitVec.smod 16)
source
@[simp]
theorem Int16.toBitVec_and (a b : Int16) :
(a &&& b).toBitVec = a.toBitVec &&& b.toBitVec
source
@[simp]
theorem Int16.toBitVec_abs (a : Int16) :
a.abs.toBitVec = a.toBitVec.abs
source
@[simp]
theorem Int16.toBitVec_sub {a b : Int16} :
(a - b).toBitVec = a.toBitVec - b.toBitVec
source
@[simp]
theorem Int16.toBitVec_mul {a b : Int16} :
(a * b).toBitVec = a.toBitVec * b.toBitVec
source
@[simp]
theorem Int32.toBitVec_div {a b : Int32} :
(a / b).toBitVec = a.toBitVec.sdiv b.toBitVec
source
@[simp]
theorem Int32.toBitVec_xor (a b : Int32) :
(a ^^^ b).toBitVec = a.toBitVec ^^^ b.toBitVec
source
@[simp]
theorem Int32.toBitVec_and (a b : Int32) :
(a &&& b).toBitVec = a.toBitVec &&& b.toBitVec
source
@[simp]
theorem Int32.toBitVec_shiftLeft (a b : Int32) :
(a <<< b).toBitVec = a.toBitVec <<< b.toBitVec.smod 32
source
@[simp]
theorem Int32.toBitVec_shiftRight (a b : Int32) :
(a >>> b).toBitVec = a.toBitVec.sshiftRight' (b.toBitVec.smod 32)
source
@[simp]
theorem Int32.toBitVec_mod {a b : Int32} :
(a % b).toBitVec = a.toBitVec.srem b.toBitVec
source
@[simp]
theorem Int32.toBitVec_not {a : Int32} :
(~~~a).toBitVec = ~~~a.toBitVec
source
@[simp]
theorem Int32.toBitVec_add {a b : Int32} :
(a + b).toBitVec = a.toBitVec + b.toBitVec
source
@[simp]
theorem Int32.toBitVec_mul {a b : Int32} :
(a * b).toBitVec = a.toBitVec * b.toBitVec
source
@[simp]
theorem Int32.toBitVec_abs (a : Int32) :
a.abs.toBitVec = a.toBitVec.abs
source
@[simp]
theorem Int32.toBitVec_or (a b : Int32) :
(a ||| b).toBitVec = a.toBitVec ||| b.toBitVec
source
@[simp]
theorem Int32.toBitVec_sub {a b : Int32} :
(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
@[simp]
theorem Int64.toBitVec_add {a b : Int64} :
(a + b).toBitVec = a.toBitVec + b.toBitVec
source
@[simp]
theorem Int64.toBitVec_sub {a b : Int64} :
(a - b).toBitVec = a.toBitVec - b.toBitVec
source
@[simp]
theorem Int64.toBitVec_abs (a : Int64) :
a.abs.toBitVec = a.toBitVec.abs
source
@[simp]
theorem Int64.toBitVec_shiftRight (a b : Int64) :
(a >>> b).toBitVec = a.toBitVec.sshiftRight' (b.toBitVec.smod 64)
source
@[simp]
theorem Int64.toBitVec_and (a b : Int64) :
(a &&& b).toBitVec = a.toBitVec &&& b.toBitVec
source
@[simp]
theorem Int64.toBitVec_not {a : Int64} :
(~~~a).toBitVec = ~~~a.toBitVec
source
@[simp]
theorem Int64.toBitVec_or (a b : Int64) :
(a ||| b).toBitVec = a.toBitVec ||| b.toBitVec
source
@[simp]
theorem Int64.toBitVec_shiftLeft (a b : Int64) :
(a <<< b).toBitVec = a.toBitVec <<< b.toBitVec.smod 64
source
@[simp]
theorem Int64.toBitVec_div {a b : Int64} :
(a / b).toBitVec = a.toBitVec.sdiv b.toBitVec
source
@[simp]
theorem Int64.toBitVec_mul {a b : Int64} :
(a * b).toBitVec = a.toBitVec * b.toBitVec
source
@[simp]
theorem Int64.toBitVec_xor (a b : Int64) :
(a ^^^ b).toBitVec = a.toBitVec ^^^ b.toBitVec
source
@[simp]
theorem ISize.toBitVec_shiftLeft (a b : ISize) :
(a <<< b).toBitVec = a.toBitVec <<< b.toBitVec.smod ↑System.Platform.numBits
source
@[simp]
theorem ISize.toBitVec_not {a : ISize} :
(~~~a).toBitVec = ~~~a.toBitVec
source
@[simp]
theorem ISize.toBitVec_shiftRight (a b : ISize) :
(a >>> b).toBitVec = a.toBitVec.sshiftRight' (b.toBitVec.smod ↑System.Platform.numBits)
source
@[simp]
theorem ISize.toBitVec_mod {a b : ISize} :
(a % b).toBitVec = a.toBitVec.srem b.toBitVec
source
@[simp]
theorem ISize.toBitVec_abs (a : ISize) :
a.abs.toBitVec = a.toBitVec.abs
source
@[simp]
theorem ISize.toBitVec_div {a b : ISize} :
(a / b).toBitVec = a.toBitVec.sdiv b.toBitVec
source
@[simp]
theorem ISize.toBitVec_mul {a b : ISize} :
(a * b).toBitVec = 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_and (a b : ISize) :
(a &&& b).toBitVec = a.toBitVec &&& b.toBitVec
source
@[simp]
theorem ISize.toBitVec_xor (a b : ISize) :
(a ^^^ b).toBitVec = a.toBitVec ^^^ b.toBitVec
source
@[simp]
theorem ISize.toBitVec_sub {a b : ISize} :
(a - b).toBitVec = a.toBitVec - b.toBitVec
source
@[simp]
theorem ISize.toBitVec_or (a b : ISize) :
(a ||| b).toBitVec = a.toBitVec ||| b.toBitVec
source
@[simp]
theorem Bool.toBitVec_toInt8 {b : Bool} :
b.toInt8.toBitVec = BitVec.setWidth 8 (BitVec.ofBool b)
source
@[simp]
theorem Bool.toBitVec_toInt16 {b : Bool} :
b.toInt16.toBitVec = BitVec.setWidth 16 (BitVec.ofBool b)
source
@[simp]
theorem Bool.toBitVec_toInt32 {b : Bool} :
b.toInt32.toBitVec = BitVec.setWidth 32 (BitVec.ofBool b)
source
@[simp]
theorem Bool.toBitVec_toInt64 {b : Bool} :
b.toInt64.toBitVec = BitVec.setWidth 64 (BitVec.ofBool b)
source
@[simp]
theorem Bool.toBitVec_toISize {b : Bool} :
b.toISize.toBitVec = BitVec.setWidth System.Platform.numBits (BitVec.ofBool b)