mathlib documentation

data.lazy_list

Lazy lists #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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) :

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

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

The singleton lazy list.

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

Constructs a lazy list from a list.

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

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

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} :

Zips two lazy lists.

Equations

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.filter {α : Type u} (p : α Prop) [decidable_pred p] :

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, ...]