Lemmas about bitwise operations on integers. #
Possibly only of archaeological significance.
testBit m n
returns whether the (n+1)ˢᵗ
least significant bit is 1
or 0
Equations
- Int.testBit x x = match x, x with | Int.ofNat m, n => Nat.testBit m n | Int.negSucc m, n => !Nat.testBit m n
Int.natBitwise
is an auxiliary definition for Int.bitwise
.
Equations
- Int.natBitwise f m n = bif f false false then Int.negSucc (Nat.bitwise' (fun x y => !f x y) m n) else ↑(Nat.bitwise' f m n)
Int.bitwise
applies the function f
to pairs of bits in the same position in
the binary representations of its inputs.
Equations
- One or more equations did not get rendered due to their size.
shiftr m n
produces a integer whose binary representation
is obtained by right-shifting the binary representation of m
by n
places
Equations
- Int.shiftr m n = Int.shiftl m (-n)