Lemmas about bitwise operations on integers. #
Possibly only of archaeological significance.
Int.natBitwise
is an auxiliary definition for Int.bitwise
.
Instances For
Int.bitwise
applies the function f
to pairs of bits in the same position in
the binary representations of its inputs.
Instances For
m <<< n
produces an integer whose binary representation
is obtained by left-shifting the binary representation of m
by n
places
m >>> n
produces an integer whose binary representation
is obtained by right-shifting the binary representation of m
by n
places