Documentation

Mathlib.Init.Data.List.Lemmas

Lemmas for List not (yet) in Std

def List.mapAccumr {σ : Type w₂} {α : Type u_1} {β : Type u_2} (f : ασσ × β) :
List ασσ × List β

Runs a function over a list returning the intermediate results and a a final result.

Equations
@[simp]
theorem List.length_mapAccumr {σ : Type w₂} {α : Type u_1} {β : Type u_2} (f : ασσ × β) (x : List α) (s : σ) :

Length of the list obtained by mapAccumr.

def List.mapAccumr₂ {φ : Type w₁} {σ : Type w₂} {α : Type u_1} {β : Type u_2} (f : αβσσ × φ) :
List αList βσσ × List φ

Runs a function over two lists returning the intermediate results and a a final result.

Equations
@[simp]
theorem List.length_mapAccumr₂ {φ : Type w₁} {σ : Type w₂} {α : Type u_1} {β : Type u_2} (f : αβσσ × φ) (x : List α) (y : List β) (c : σ) :

Length of a list obtained using mapAccumr₂.