Documentation

Init.Data.BitVec.Folds

def BitVec.iunfoldr {w : Nat} {α : Type u_1} (f : Fin wαα × Bool) (s : α) :
α × BitVec w

iunfoldr is an iterative operation that applies a function f repeatedly.

It produces a sequence of state values [s_0, s_1 .. s_w] and a bitvector v where f i s_i = (s_{i+1}, b_i) and b_i is bit ith least-significant bit in v (e.g., getLsb v i = b_i).

Theorems involving iunfoldr can be eliminated using iunfoldr_replace below.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    theorem BitVec.iunfoldr.fst_eq {w : Nat} {α : Type u_1} {f : Fin wαα × Bool} (state : Natα) (s : α) (init : s = state 0) (ind : ∀ (i : Fin w), (f i (state i)).fst = state (i + 1)) :
    (BitVec.iunfoldr f s).fst = state w
    theorem BitVec.iunfoldr_replace {w : Nat} {α : Type u_1} {f : Fin wαα × Bool} (state : Natα) (value : BitVec w) (a : α) (init : state 0 = a) (step : ∀ (i : Fin w), f i (state i) = (state (i + 1), BitVec.getLsb value i)) :
    BitVec.iunfoldr f a = (state w, value)

    Correctness theorem for iunfoldr.