mathlib3 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 α.)

source
inductive lazy_list (α : Type u) :
Type u

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

Instances for lazy_list
source
@[protected, instance]
def lazy_list.inhabited {α : Type u} :
inhabited (lazy_list α)
Equations
source
def lazy_list.singleton {α : Type u} :
α → lazy_list α

The singleton lazy list.

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

Constructs a lazy list from a list.

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

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

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

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

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

Removes the first element of the lazy list.

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

Appends two lazy lists.

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

Maps a function over a lazy list.

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

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

Equations
source
def lazy_list.zip {α : Type u} {β : Type v} :
lazy_list α → lazy_list β → lazy_list (α × β)

Zips two lazy lists.

Equations
source
def lazy_list.join {α : Type u} :
lazy_list (lazy_list α) → lazy_list α

The monadic join operation for lazy lists.

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

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

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

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

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

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
source
def lazy_list.nth {α : Type u} :
lazy_list α → ℕ → option α

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

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

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.

source
meta def lazy_list.iota (i : ℕ) :
lazy_list ℕ

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