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