English
Runs a function over a vector returning the intermediate results and a final result: mapAccumr (f) (⟨x,px⟩) c = ⟨s, ⟨y,py⟩⟩, where (s,y) = List.mapAccumr f x c.
Русский
Проходит по вектору и возвращает промежуточные результаты и итоговый: mapAccumr(f)(⟨x,px⟩)(c) = ⟨s, ⟨y,py⟩⟩, где (s,y) = List.mapAccumr f x c.
LaTeX
$$$\\mathrm{mapAccumr}(f) : \\text{Vector }\\alpha n \\to \\sigma \\to (\\sigma \\times \\text{Vector }\\beta n)$ and $\\mathrm{mapAccumr}(f)(\\langle x,px\\rangle)(c) = \\langle s,\\langle y,py\\rangle\\rangle$ with $(s,y) = \\mathrm{List.mapAccumr} f\, x\, c$$$
Lean4
/-- Vector of length `n` from a function on `Fin n`. -/
def ofFn : ∀ {n}, (Fin n → α) → Vector α n
| 0, _ => nil
| _ + 1, f => cons (f 0) (ofFn fun i ↦ f i.succ)
