HepLean 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.and_toNat (a : UInt8) (b : UInt8) :
    (a &&& b).toNat = a.toNat &&& b.toNat
    source
    @[simp]
    theorem UInt16.and_toNat (a : UInt16) (b : UInt16) :
    (a &&& b).toNat = a.toNat &&& b.toNat
    source
    @[simp]
    theorem UInt32.and_toNat (a : UInt32) (b : UInt32) :
    (a &&& b).toNat = a.toNat &&& b.toNat
    source
    @[simp]
    theorem UInt64.and_toNat (a : UInt64) (b : UInt64) :
    (a &&& b).toNat = a.toNat &&& b.toNat
    source
    @[simp]
    theorem USize.and_toNat (a : USize) (b : USize) :
    (a &&& b).toNat = a.toNat &&& b.toNat