Possibly only of archaeological significance.
div2 n = n/2
bodd n returns true if n is odd
bit b appends the digit b to the binary representation of
its integer input.
testBit m n returns whether the (n+1)ˢᵗ least significant bit is 1 or 0
testBit m n
Int.natBitwise is an auxiliary definition for Int.bitwise.
Int.bitwise applies the function f to pairs of bits in the same position in
the binary representations of its inputs.
lnot flips all the bits in the binary representation of its input
lor takes two integers and returns their bitwise or
land takes two integers and returns their bitwise and
ldiff' a b performs bitwise set difference. For each corresponding
pair of bits taken as booleans, say aᵢ and bᵢ, it applies the
boolean operation aᵢ ∧ bᵢ to obtain the iᵗʰ bit of the result.
ldiff' a b
aᵢ ∧ bᵢ
lxor' computes the bitwise xor of two natural numbers
m <<< n produces an integer whose binary representation
is obtained by left-shifting the binary representation of m by n places
m <<< n
m >>> n produces an integer whose binary representation
is obtained by right-shifting the binary representation of m by n places
m >>> n