English
Runs a function over a pair of vectors, returning the intermediate results and a final result: mapAccumr₂ (f) v w c = ⟨s, ⟨t, pt⟩⟩ with s,t from List.mapAccumr₂ f x y c.
Русский
Проходит по паре векторов и возвращает промежуточные и итоговые результаты: mapAccumr₂(f) v w c = ⟨s, ⟨t, pt⟩⟩.
LaTeX
$$$\\mathrm{mapAccumr\\_2}(f) : \\text{Vector }\\alpha n \\to \\text{Vector }\\beta n \\to \\sigma \\to (\\sigma \\times \\text{Vector }\\phi n)$ with $\\langle s, \\langle t, pt\\rangle\\rangle = \\mathrm{List.mapAccumr\\_2} f x y c$$$
Lean4
/-- Create a vector from another with a provably equal length. -/
protected def congr {n m : ℕ} (h : n = m) : Vector α n → Vector α m
| ⟨x, p⟩ => ⟨x, h ▸ p⟩
