English
Let f : α → β → γ → γ × δ. mapAccumr₂ f maps two lists elementwise from right to left, producing a final γ and a list of δ, stopping when either list ends.
Русский
Пусть f : α → β → γ → γ × δ. mapAccumr₂ f сопоставляет элементы двух списков справа налево, давая итоговый γ и список δ; процесс останавливается, когда один из списков заканчивается.
LaTeX
$$$$\text{mapAccumr₂}(f)([],_,c)=(c,[]) \\ \text{mapAccumr₂}(f)(x::xr,y::yr,c)=\text{let } r=\text{mapAccumr₂}(f)(xr,yr,c)\text{ in }(q.1,q.2::r.2)\text{ где } q=f(x,y)\, r.1.$$$$
Lean4
/-- Runs a function over two lists returning the intermediate results and a final result. -/
def mapAccumr₂ (f : α → β → γ → γ × δ) : List α → List β → γ → γ × List δ
| [], _, c => (c, [])
| _, [], c => (c, [])
| x :: xr, y :: yr, c =>
let r := mapAccumr₂ f xr yr c
let q := f x y r.1
(q.1, q.2 :: r.2)
