Documentation

Init.Data.UInt.Bitwise

source
def commandDeclare_bitwise_uint_theorems__ :
Lean.ParserDescr
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem UInt8.toNat_shiftRight (a b : UInt8) :
    (a >>> b).toNat = a.toNat >>> (b.toNat % 8)
    source
    @[simp]
    theorem UInt8.toBitVec_or (a b : UInt8) :
    (a ||| b).toBitVec = a.toBitVec ||| b.toBitVec
    source
    @[deprecated UInt8.toNat_and]
    theorem UInt8.and_toNat (a b : UInt8) :
    (a &&& b).toNat = a.toNat &&& b.toNat
    source
    @[simp]
    theorem UInt8.toNat_xor (a b : UInt8) :
    (a ^^^ b).toNat = a.toNat ^^^ b.toNat
    source
    @[simp]
    theorem UInt8.toBitVec_and (a b : UInt8) :
    (a &&& b).toBitVec = a.toBitVec &&& b.toBitVec
    source
    @[simp]
    theorem UInt8.toNat_or (a b : UInt8) :
    (a ||| b).toNat = a.toNat ||| b.toNat
    source
    @[simp]
    theorem UInt8.toBitVec_shiftRight (a b : UInt8) :
    (a >>> b).toBitVec = a.toBitVec >>> (b.toBitVec % 8)
    source
    @[simp]
    theorem UInt8.toBitVec_shiftLeft (a b : UInt8) :
    (a <<< b).toBitVec = a.toBitVec <<< (b.toBitVec % 8)
    source
    @[simp]
    theorem UInt8.toNat_and (a b : UInt8) :
    (a &&& b).toNat = a.toNat &&& b.toNat
    source
    @[simp]
    theorem UInt8.toBitVec_xor (a b : UInt8) :
    (a ^^^ b).toBitVec = a.toBitVec ^^^ b.toBitVec
    source
    @[simp]
    theorem UInt8.toNat_shiftLeft (a b : UInt8) :
    (a <<< b).toNat = a.toNat <<< (b.toNat % 8) % 2 ^ 8
    source
    @[simp]
    theorem UInt16.toBitVec_shiftRight (a b : UInt16) :
    (a >>> b).toBitVec = a.toBitVec >>> (b.toBitVec % 16)
    source
    @[simp]
    theorem UInt16.toNat_xor (a b : UInt16) :
    (a ^^^ b).toNat = a.toNat ^^^ b.toNat
    source
    @[simp]
    theorem UInt16.toBitVec_and (a b : UInt16) :
    (a &&& b).toBitVec = a.toBitVec &&& b.toBitVec
    source
    @[simp]
    theorem UInt16.toNat_or (a b : UInt16) :
    (a ||| b).toNat = a.toNat ||| b.toNat
    source
    @[simp]
    theorem UInt16.toNat_shiftRight (a b : UInt16) :
    (a >>> b).toNat = a.toNat >>> (b.toNat % 16)
    source
    @[simp]
    theorem UInt16.toBitVec_or (a b : UInt16) :
    (a ||| b).toBitVec = a.toBitVec ||| b.toBitVec
    source
    @[simp]
    theorem UInt16.toBitVec_shiftLeft (a b : UInt16) :
    (a <<< b).toBitVec = a.toBitVec <<< (b.toBitVec % 16)
    source
    @[simp]
    theorem UInt16.toBitVec_xor (a b : UInt16) :
    (a ^^^ b).toBitVec = a.toBitVec ^^^ b.toBitVec
    source
    @[deprecated UInt16.toNat_and]
    theorem UInt16.and_toNat (a b : UInt16) :
    (a &&& b).toNat = a.toNat &&& b.toNat
    source
    @[simp]
    theorem UInt16.toNat_shiftLeft (a b : UInt16) :
    (a <<< b).toNat = a.toNat <<< (b.toNat % 16) % 2 ^ 16
    source
    @[simp]
    theorem UInt16.toNat_and (a b : UInt16) :
    (a &&& b).toNat = a.toNat &&& b.toNat
    source
    @[simp]
    theorem UInt32.toBitVec_shiftRight (a b : UInt32) :
    (a >>> b).toBitVec = a.toBitVec >>> (b.toBitVec % 32)
    source
    @[simp]
    theorem UInt32.toBitVec_shiftLeft (a b : UInt32) :
    (a <<< b).toBitVec = a.toBitVec <<< (b.toBitVec % 32)
    source
    @[simp]
    theorem UInt32.toNat_or (a b : UInt32) :
    (a ||| b).toNat = a.toNat ||| b.toNat
    source
    @[simp]
    theorem UInt32.toBitVec_and (a b : UInt32) :
    (a &&& b).toBitVec = a.toBitVec &&& b.toBitVec
    source
    @[simp]
    theorem UInt32.toNat_shiftLeft (a b : UInt32) :
    (a <<< b).toNat = a.toNat <<< (b.toNat % 32) % 2 ^ 32
    source
    @[simp]
    theorem UInt32.toBitVec_or (a b : UInt32) :
    (a ||| b).toBitVec = a.toBitVec ||| b.toBitVec
    source
    @[simp]
    theorem UInt32.toNat_shiftRight (a b : UInt32) :
    (a >>> b).toNat = a.toNat >>> (b.toNat % 32)
    source
    @[simp]
    theorem UInt32.toNat_and (a b : UInt32) :
    (a &&& b).toNat = a.toNat &&& b.toNat
    source
    @[deprecated UInt32.toNat_and]
    theorem UInt32.and_toNat (a b : UInt32) :
    (a &&& b).toNat = a.toNat &&& b.toNat
    source
    @[simp]
    theorem UInt32.toBitVec_xor (a b : UInt32) :
    (a ^^^ b).toBitVec = a.toBitVec ^^^ b.toBitVec
    source
    @[simp]
    theorem UInt32.toNat_xor (a b : UInt32) :
    (a ^^^ b).toNat = a.toNat ^^^ b.toNat
    source
    @[simp]
    theorem UInt64.toBitVec_shiftLeft (a b : UInt64) :
    (a <<< b).toBitVec = a.toBitVec <<< (b.toBitVec % 64)
    source
    @[simp]
    theorem UInt64.toBitVec_or (a b : UInt64) :
    (a ||| b).toBitVec = a.toBitVec ||| b.toBitVec
    source
    @[simp]
    theorem UInt64.toNat_and (a b : UInt64) :
    (a &&& b).toNat = a.toNat &&& b.toNat
    source
    @[deprecated UInt64.toNat_and]
    theorem UInt64.and_toNat (a b : UInt64) :
    (a &&& b).toNat = a.toNat &&& b.toNat
    source
    @[simp]
    theorem UInt64.toBitVec_and (a b : UInt64) :
    (a &&& b).toBitVec = a.toBitVec &&& b.toBitVec
    source
    @[simp]
    theorem UInt64.toNat_or (a b : UInt64) :
    (a ||| b).toNat = a.toNat ||| b.toNat
    source
    @[simp]
    theorem UInt64.toNat_shiftLeft (a b : UInt64) :
    (a <<< b).toNat = a.toNat <<< (b.toNat % 64) % 2 ^ 64
    source
    @[simp]
    theorem UInt64.toNat_shiftRight (a b : UInt64) :
    (a >>> b).toNat = a.toNat >>> (b.toNat % 64)
    source
    @[simp]
    theorem UInt64.toBitVec_xor (a b : UInt64) :
    (a ^^^ b).toBitVec = a.toBitVec ^^^ b.toBitVec
    source
    @[simp]
    theorem UInt64.toNat_xor (a b : UInt64) :
    (a ^^^ b).toNat = a.toNat ^^^ b.toNat
    source
    @[simp]
    theorem UInt64.toBitVec_shiftRight (a b : UInt64) :
    (a >>> b).toBitVec = a.toBitVec >>> (b.toBitVec % 64)
    source
    @[simp]
    theorem USize.toBitVec_shiftLeft (a b : USize) :
    (a <<< b).toBitVec = a.toBitVec <<< (b.toBitVec % ↑System.Platform.numBits)
    source
    @[simp]
    theorem USize.toNat_xor (a b : USize) :
    (a ^^^ b).toNat = a.toNat ^^^ b.toNat
    source
    @[simp]
    theorem USize.toBitVec_xor (a b : USize) :
    (a ^^^ b).toBitVec = a.toBitVec ^^^ b.toBitVec
    source
    @[simp]
    theorem USize.toBitVec_shiftRight (a b : USize) :
    (a >>> b).toBitVec = a.toBitVec >>> (b.toBitVec % ↑System.Platform.numBits)
    source
    @[simp]
    theorem USize.toNat_shiftRight (a b : USize) :
    (a >>> b).toNat = a.toNat >>> (b.toNat % System.Platform.numBits)
    source
    @[simp]
    theorem USize.toNat_or (a b : USize) :
    (a ||| b).toNat = a.toNat ||| b.toNat
    source
    @[simp]
    theorem USize.toNat_and (a b : USize) :
    (a &&& b).toNat = a.toNat &&& b.toNat
    source
    @[deprecated USize.toNat_and]
    theorem USize.and_toNat (a b : USize) :
    (a &&& b).toNat = a.toNat &&& b.toNat
    source
    @[simp]
    theorem USize.toNat_shiftLeft (a b : USize) :
    (a <<< b).toNat = a.toNat <<< (b.toNat % System.Platform.numBits) % 2 ^ System.Platform.numBits
    source
    @[simp]
    theorem USize.toBitVec_and (a b : USize) :
    (a &&& b).toBitVec = a.toBitVec &&& b.toBitVec
    source
    @[simp]
    theorem USize.toBitVec_or (a b : USize) :
    (a ||| b).toBitVec = a.toBitVec ||| b.toBitVec