This module exists to provide the very basic BitVec
definitions required for
Init.Data.UInt.BasicAux
.
Equations
- BitVec.instOfNat = { ofNat := BitVec.ofNat n i }
Equations
- BitVec.instAdd = { add := BitVec.add }
Equations
- BitVec.instSub = { sub := BitVec.sub }