English
Let f : α → γ → γ × β. mapAccumr f maps a list of α to a pair (γ, List β) by processing elements from right to left: the final γ is obtained by folding f over the list with an initial accumulator, and the resulting β-values are collected in a list in the same left-to-right order as the input.
Русский
Пусть f : α → γ → γ × β. mapAccumr f отображает список α в пару (γ, List β), обрабатывая элементы справа налево: итоговый γ получается как аккумулятор при свёртке списка, а значения β собираются в список в том же порядке, что и входной список.
LaTeX
$$$$\text{mapAccumr}(f)([],c)=(c,[]) \\ \text{mapAccumr}(f)(y:\\ yr,c)=(\text{fst}(f(y,\text{snd}(\text{mapAccumr}(f)(yr,c)) )),\text{cons}(\text{snd}(\text{mapAccumr}(f)(yr,c))))$$$$
Lean4
/-- Runs a function over a list returning the intermediate results and a final result. -/
def mapAccumr (f : α → γ → γ × β) : List α → γ → γ × List β
| [], c => (c, [])
| y :: yr, c =>
let r := mapAccumr f yr c
let z := f y r.1
(z.1, z.2 :: r.2)
