@[irreducible]
def
Fin.hIterateFrom
(P : Nat → Sort u_1)
{n : Nat}
(f : (i : Fin n) → P ↑i → P (↑i + 1))
(i : Nat)
(ubnd : i ≤ n)
(a : P i)
:
P n
hIterateFrom f i bnd a applies f over indices [i:n] to compute P n
from P i.
See hIterate below for more details.
Equations
- Fin.hIterateFrom P f i ubnd a = if g : i < n then Fin.hIterateFrom P f (i + 1) g (f ⟨i, g⟩ a) else let_fun p := ⋯; cast ⋯ a
def
Fin.hIterate
(P : Nat → Sort u_1)
{n : Nat}
(init : P 0)
(f : (i : Fin n) → P ↑i → P (↑i + 1))
:
P n
hIterate is a heterogeneous iterative operation that applies a
index-dependent function f to a value init : P start a total of
stop - start times to produce a value of type P stop.
Concretely, hIterate start stop f init is equal to
init |> f start _ |> f (start+1) _ ... |> f (end-1) _
Because it is heterogeneous and must return a value of type P stop,
hIterate requires proof that start ≤ stop.
One can prove properties of hIterate using the general theorem
hIterate_elim or other more specialized theorems.
Equations
- Fin.hIterate P init f = Fin.hIterateFrom P f 0 ⋯ init