mathlib documentation

core.data.lazy_list

inductive lazy_list  :
Type uType 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} :
(α → β)lazy_list αlazy_list β

Equations
def lazy_list.map₂ {α : Type u} {β : Type v} {δ : Type w} :
(α → β → δ)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} :
lazy_list α(α → β)lazy_list β

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} :
(α → α)α → lazy_list α