mathlib3 documentation


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

The singleton lazy list.

def lazy_list.of_list {α : Type u} :

Constructs a lazy list from a list.

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.

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

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

def lazy_list.tail {α : Type u} :

Removes the first element of the lazy list.


Appends two lazy lists.

def {α : Type u} {β : Type v} (f : α β) :

Maps a function over a lazy list.

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

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

def {α : Type u} {β : Type v} :

Zips two lazy lists.


The monadic join operation for lazy lists.

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

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

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.

def lazy_list.nth {α : Type u} :

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

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