This module exists to provide the very basic BitVec
definitions required for
Init.Data.UInt.BasicAux
.
@[match_pattern]
The bitvector with value i mod 2^n
.
Conventions for notations in identifiers:
The recommended spelling of
0#n
in identifiers iszero
(notofNat_zero
).The recommended spelling of
1#n
in identifiers isone
(notofNat_one
).
Equations
Instances For
Adds two bitvectors. This can be interpreted as either signed or unsigned addition modulo 2^n
.
Usually accessed via the +
operator.
SMT-LIB name: bvadd
.
Equations
Instances For
Subtracts one bitvector from another. This can be interpreted as either signed or unsigned subtraction
modulo 2^n
. Usually accessed via the -
operator.