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

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

• nil: {α : Type u} →

The empty lazy list.

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

Construct a lazy list from an element and a tail inside a thunk.

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

The singleton lazy list.

Equations
Instances For
def LazyList.ofList {α : Type u_1} :
List α

Constructs a lazy list from a list.

Equations
Instances For
def LazyList.toList {α : Type u_1} :
List α

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

Equations
Instances For
def LazyList.headI {α : Type u_1} [] :
α

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

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

Removes the first element of the lazy list.

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

Appends two lazy lists.

Equations
Instances For
def LazyList.map {α : Type u_1} {β : Type u_2} (f : αβ) :

Maps a function over a lazy list.

Equations
Instances For
def LazyList.map₂ {α : Type u_1} {β : Type u_2} {δ : Type u_3} (f : αβδ) :

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

Equations
Instances For
def LazyList.zip {α : Type u_1} {β : Type u_2} :
LazyList (α × β)

Zips two lazy lists.

Equations
Instances For
def LazyList.join {α : Type u_1} :
LazyList ()

The monadic join operation for lazy lists.

Equations
Instances For
def LazyList.take {α : Type u_1} :
NatList α

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

Equations
Instances For
def LazyList.filter {α : Type u_1} (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
Instances For
def LazyList.get? {α : Type u_1} :
Nat

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

Equations
Instances For
partial def LazyList.iterates {α : Type u_1} (f : αα) :
α

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

def LazyList.iota (i : Nat) :

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

Equations
Instances For