HepLean Documentation
Init
.
Data
.
UInt
.
Bitwise
Search
Google site search
return to top
source
Imports
Init.Data.BitVec.Lemmas
Init.Data.Fin.Bitwise
Init.Data.UInt.Basic
Imported by
commandDeclare_bitwise_uint_theorems_
UInt8
.
and_toNat
UInt16
.
and_toNat
UInt32
.
and_toNat
UInt64
.
and_toNat
USize
.
and_toNat
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 b :
UInt8
)
:
(
a
&&&
b
)
.toNat
=
a
.toNat
&&&
b
.toNat
source
@[simp]
theorem
UInt16
.
and_toNat
(a b :
UInt16
)
:
(
a
&&&
b
)
.toNat
=
a
.toNat
&&&
b
.toNat
source
@[simp]
theorem
UInt32
.
and_toNat
(a b :
UInt32
)
:
(
a
&&&
b
)
.toNat
=
a
.toNat
&&&
b
.toNat
source
@[simp]
theorem
UInt64
.
and_toNat
(a b :
UInt64
)
:
(
a
&&&
b
)
.toNat
=
a
.toNat
&&&
b
.toNat
source
@[simp]
theorem
USize
.
and_toNat
(a b :
USize
)
:
(
a
&&&
b
)
.toNat
=
a
.toNat
&&&
b
.toNat