Lemmas about bitwise operations on natural numbers. #
Possibly only of archaeological significance.
boddDiv2 n
returns a 2-tuple of type (Bool,Nat)
where the Bool
value indicates whether n
is odd or not
and the Nat
value returns ⌊n/2⌋
Equations
- Nat.boddDiv2 0 = (false, 0)
- Nat.boddDiv2 (Nat.succ n) = match Nat.boddDiv2 n with | (false, m) => (true, m) | (true, m) => (false, Nat.succ m)
Instances For
shiftLeft' b m n
performs a left shift of m
n
times
and adds the bit b
as the least significant bit each time.
Returns the corresponding natural number
Equations
- Nat.shiftLeft' b m 0 = m
- Nat.shiftLeft' b m (Nat.succ n) = Nat.bit b (Nat.shiftLeft' b m n)
Instances For
Std4 takes the unprimed name for Nat.shiftLeft_eq m n : m <<< n = m * 2 ^ n
.
A recursion principle for bit
representations of natural numbers.
For a predicate C : Nat → Sort*
, if instances can be
constructed for natural numbers of the form bit b n
,
they can be constructed for all natural numbers.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Nat.bitwise'
(different from Nat.bitwise
in Lean 4 core)
applies the function f
to pairs of bits in the same position in
the binary representations of its inputs.
Instances For
bitwise ops