mathlib documentation

core / data.lazy_list

inductive lazy_list (α : Type u) :
Type u

def lazy_list.singleton {α : Type u} :
α → lazy_list α

Equations
def lazy_list.to_list {α : Type u} :
lazy_list αlist α

Equations
def lazy_list.head {α : Type u} [inhabited α] :
lazy_list α → α

Equations
def lazy_list.tail {α : Type u} :

Equations
def lazy_list.append {α : Type u} :
lazy_list αthunk (lazy_list α)lazy_list α

Equations
def lazy_list.map {α : Type u} {β : Type v} (f : α → β) :

Equations
def lazy_list.map₂ {α : Type u} {β : Type v} {δ : Type w} (f : α → β → δ) :
lazy_list αlazy_list βlazy_list δ

Equations
def lazy_list.zip {α : Type u} {β : Type v} :
lazy_list αlazy_list βlazy_list × β)

Equations
def lazy_list.join {α : Type u} :

Equations
def lazy_list.for {α : Type u} {β : Type v} (l : lazy_list α) (f : α → β) :

Equations
def lazy_list.filter {α : Type u} (p : α → Prop) [decidable_pred p] :

Equations
def lazy_list.nth {α : Type u} :
lazy_list αoption α

Equations
meta def lazy_list.iterates {α : Type u} (f : α → α) :
α → lazy_list α

meta def lazy_list.iota (i : ) :