Documentation
Init
.
GrindInstances
.
Ring
.
BitVec
Search
return to top
source
Imports
Init.Grind.ToInt
Init.GrindInstances.ToInt
Init.Data.BitVec.Basic
Init.Data.BitVec.Bootstrap
Init.Data.BitVec.Lemmas
Init.Grind.Ring.Basic
Init.Grind.Ring.ToInt
Imported by
Lean
.
Grind
.
instCommRingBitVec
Lean
.
Grind
.
instIsCharPBitVecHPowNatOfNat
Lean
.
Grind
.
instPowBitVecUint
source
@[instance_reducible]
instance
Lean
.
Grind
.
instCommRingBitVec
{
w
:
Nat
}
:
CommRing
(
BitVec
w
)
source
instance
Lean
.
Grind
.
instIsCharPBitVecHPowNatOfNat
{
w
:
Nat
}
:
IsCharP
(
BitVec
w
)
(
2
^
w
)
source
instance
Lean
.
Grind
.
instPowBitVecUint
{
w
:
Nat
}
:
ToInt.Pow
(
BitVec
w
)
(
IntInterval.uint
w
)