Runs a function over a list returning the intermediate results and a a final result.
Equations
- List.mapAccumr f [] x = (x, [])
- List.mapAccumr f (y :: yr) x = let r := List.mapAccumr f yr x; let z := f y r.fst; (z.fst, z.snd :: r.snd)
@[simp]
theorem
List.length_mapAccumr
{σ : Type w₂}
{α : Type u_1}
{β : Type u_2}
(f : α → σ → σ × β)
(x : List α)
(s : σ)
:
List.length (List.mapAccumr f x s).snd = List.length x
Length of the list obtained by mapAccumr.
def
List.mapAccumr₂
{φ : Type w₁}
{σ : Type w₂}
{α : Type u_1}
{β : Type u_2}
(f : α → β → σ → σ × φ)
:
Runs a function over two lists returning the intermediate results and a a final result.
Equations
- List.mapAccumr₂ f [] x x = (x, [])
- List.mapAccumr₂ f x [] x = (x, [])
- List.mapAccumr₂ f (x_3 :: xr) (y :: yr) x = let r := List.mapAccumr₂ f xr yr x; let q := f x_3 y r.fst; (q.fst, q.snd :: r.snd)
@[simp]
theorem
List.length_mapAccumr₂
{φ : Type w₁}
{σ : Type w₂}
{α : Type u_1}
{β : Type u_2}
(f : α → β → σ → σ × φ)
(x : List α)
(y : List β)
(c : σ)
:
List.length (List.mapAccumr₂ f x y c).snd = min (List.length x) (List.length y)
Length of a list obtained using mapAccumr₂.