# Documentation

Mathlib.Data.LazyList

# Lazy lists #

The type LazyList α is a lazy list with elements of type α. In the VM, these are potentially infinite lists where all elements after the first are computed on-demand. (This is only useful for execution in the VM, logically we can prove that LazyList α is isomorphic to List α.)

inductive LazyList (α : Type u) :
• nil: {α : Type u} →
• cons: {α : Type u} → αThunk ()

Lazy list. All elements (except the first) are computed lazily.

Instances For
Equations
• LazyList.instInhabitedLazyList = { default := LazyList.nil }
def LazyList.singleton {α : Type u} :
α

The singleton lazy list.

Equations
def LazyList.ofList {α : Type u} :
List α

Constructs a lazy list from a list.

Equations
def LazyList.toList {α : Type u} :
List α

Converts a lazy list to a list. If the lazy list is infinite, then this function does not terminate.

Equations
def LazyList.headI {α : Type u} [inst : ] :
α

Returns the first element of the lazy list, or default if the lazy list is empty.

Equations
• = match x with | LazyList.nil => default | => h
def LazyList.tail {α : Type u} :

Removes the first element of the lazy list.

Equations
• = match x with | LazyList.nil => LazyList.nil | =>
def LazyList.append {α : Type u} :
Thunk ()

Appends two lazy lists.

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

Maps a function over a lazy list.

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

Maps a binary function over two lazy list. Like lazy_list.zip, the result is only as long as the smaller input.

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

Zips two lazy lists.

Equations
def LazyList.join {α : Type u} :
LazyList ()

The monadic join operation for lazy lists.

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

Maps a function over a lazy list. Same as lazy_list.map, but with swapped arguments.

Equations
def LazyList.approx {α : Type u} :
NatList α

The list containing the first n elements of a lazy list.

Equations
def LazyList.filter {α : Type u} (p : αProp) [inst : ] :

The lazy list of all elements satisfying the predicate. If the lazy list is infinite and none of the elements satisfy the predicate, then this function will not terminate.

Equations
def LazyList.nth {α : Type u} :
Nat

The nth element of a lazy list as an option (like list.nth).

Equations
unsafe def LazyList.iterates {α : Type u} (f : αα) :
α

The infinite lazy list [x, f x, f (f x), ...] of iterates of a function. This definition is meta because it creates an infinite list.

Equations
unsafe def LazyList.iota (i : Nat) :

The infinite lazy list [i, i+1, i+2, ...]

Equations