English
MapAccumr runs a function over a vector, returning the intermediate state and a vector of results.
Русский
MapAccumr последовательно применяет функцию к векторy, возвращая промежуточное состояние и вектор результатов.
LaTeX
$$$\mathrm{mapAccumr}: (\alpha\to \sigma\to \sigma\times \beta) \to \mathrm{Vector}\;\alpha\;n \to \sigma \to \sigma\times \mathrm{Vector}\;\beta\;n$$$
Lean4
/-- Runs a function over a vector returning the intermediate results and a
final result.
-/
def mapAccumr (f : α → σ → σ × β) : Vector α n → σ → σ × Vector β n
| ⟨x, px⟩, c =>
let res := List.mapAccumr f x c
⟨res.1, res.2, by simp [*, res]⟩