mapAccumr — Mathlib

English

MapAccumr runs a function over a vector, returning the intermediate state and a vector of results.

Русский

MapAccumr последовательно применяет функцию к векторy, возвращая промежуточное состояние и вектор результатов.

LaTeX

$$$\mathrm{mapAccumr}: (\alpha\to \sigma\to \sigma\times \beta) \to \mathrm{Vector}\;\alpha\;n \to \sigma \to \sigma\times \mathrm{Vector}\;\beta\;n$$$

Lean4

/-- Runs a function over a vector returning the intermediate results and a
final result.
-/
def mapAccumr (f : α → σ → σ × β) : Vector α n → σ → σ × Vector β n
  | ⟨x, px⟩, c =>
    let res := List.mapAccumr f x c
    ⟨res.1, res.2, by simp [*, res]⟩

Похожие утверждения