English
For a function f that updates a state and returns a new value, mapping over (x :: xs) with initial state s yields a pair whose first component is the updated state and whose second component is the vector built by consing the mapped head onto the tail’s result.
Русский
Для функции, которая обновляет состояние и возвращает новое значение, отображение над (x :: xs) с начальными данными s даёт пару, первая компонента — обновлённое состояние, вторая — вектор со вставленным головой в начало результата хвоста.
LaTeX
$$$\\mathrm{mapAccumr}\\; f \\; (x \\;::ᵥ\\; xs)\\; s = \\n let\\ r := \\mathrm{mapAccumr}\\; f\\; xs\\; s\\n let\\ q := f\\ x\\ r.1\\n (q.1, q.2 ::ᵥ r.2)$$$
Lean4
@[simp]
theorem mapAccumr_cons {f : α → σ → σ × β} :
mapAccumr f (x ::ᵥ xs) s =
let r := mapAccumr f xs s
let q := f x r.1
(q.1, q.2 ::ᵥ r.2) :=
rfl
