data.lazy_list

# Lazy lists #

The type lazy_list α 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 lazy_list α is isomorphic to list α.)

inductive lazy_list (α : Type u) :
Type u
• nil : Π (α : Type u),
• cons : Π (α : Type u), α → thunk (lazy_list α)

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

@[protected, instance]
def lazy_list.inhabited {α : Type u} :
Equations
def lazy_list.singleton {α : Type u} :
α →

The singleton lazy list.

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

Constructs a lazy list from a list.

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

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

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

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

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

Removes the first element of the lazy list.

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

Appends two lazy lists.

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

Maps a function over a lazy list.

Equations
def lazy_list.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 lazy_list.zip {α : Type u} {β : Type v} :
lazy_list × β)

Zips two lazy lists.

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

The monadic join operation for lazy lists.

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

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

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

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

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

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 lazy_list.nth {α : Type u} :

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

Equations
meta def lazy_list.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.

meta def lazy_list.iota (i : ) :

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