mathlib documentation

def lazy_list.singleton {α : Type u} (a : α) :

def lazy_list.of_list {α : Type u} (a : list α) :

def lazy_list.to_list {α : Type u} (a : lazy_list α) :

def lazy_list.head {α : Type u} [inhabited α] (a : lazy_list α) :

def lazy_list.tail {α : Type u} (a : lazy_list α) :

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

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

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

def lazy_list.zip {α : Type u} {β : Type v} (a : lazy_list α) (a_1 : lazy_list β) :

def lazy_list.join {α : Type u} (a : lazy_list (lazy_list α)) :

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

def lazy_list.approx {α : Type u} (a : ℕ) (a_1 : lazy_list α) :

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

def lazy_list.nth {α : Type u} (a : lazy_list α) (a_1 : ℕ) :

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

meta def lazy_list.iota (i : ℕ) :