Documentation

Mathlib.Data.LazyList

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

nil: {α : Type u} → LazyList α
cons: {α : Type u} → α → Thunk (LazyList α) → LazyList α

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

Instances For

instance LazyList.instInhabitedLazyList {α : Type u} :

Inhabited (LazyList α)

Equations

LazyList.instInhabitedLazyList = { default := LazyList.nil }

def LazyList.singleton {α : Type u} :

α → LazyList α

The singleton lazy list.

Equations

LazyList.singleton x = let a := x; LazyList.cons a (Thunk.pure LazyList.nil)

def LazyList.ofList {α : Type u} :

List α → LazyList α

Constructs a lazy list from a list.

Equations

LazyList.ofList [] = LazyList.nil
LazyList.ofList (h :: t) = LazyList.cons h { fn := fun x => LazyList.ofList t }

def LazyList.toList {α : Type u} :

LazyList α → List α

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

Equations

LazyList.toList LazyList.nil = []
LazyList.toList (LazyList.cons h t) = h :: LazyList.toList (Thunk.get t)

def LazyList.headI {α : Type u} [inst : Inhabited α] :

LazyList α → α

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

Equations

LazyList.headI x = match x with | LazyList.nil => default | LazyList.cons h tl => h

def LazyList.tail {α : Type u} :

LazyList α → LazyList α

Removes the first element of the lazy list.

Equations

LazyList.tail x = match x with | LazyList.nil => LazyList.nil | LazyList.cons hd t => Thunk.get t

def LazyList.append {α : Type u} :

LazyList α → Thunk (LazyList α) → LazyList α

Appends two lazy lists.

Equations

LazyList.append LazyList.nil x = Thunk.get x
LazyList.append (LazyList.cons h t) x = LazyList.cons h { fn := fun x => LazyList.append (Thunk.get t) x }

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

LazyList α → LazyList β

Maps a function over a lazy list.

Equations

LazyList.map f LazyList.nil = LazyList.nil
LazyList.map f (LazyList.cons h t) = LazyList.cons (f h) { fn := fun x => LazyList.map f (Thunk.get t) }

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

LazyList α → LazyList β → LazyList δ

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

Equations

LazyList.map₂ f LazyList.nil x = LazyList.nil
LazyList.map₂ f x LazyList.nil = LazyList.nil
LazyList.map₂ f (LazyList.cons h₁ t₁) (LazyList.cons h₂ t₂) = LazyList.cons (f h₁ h₂) { fn := fun x => LazyList.map₂ f (Thunk.get t₁) (Thunk.get t₂) }

def LazyList.zip {α : Type u} {β : Type v} :

LazyList α → LazyList β → LazyList (α × β)

Zips two lazy lists.

Equations

LazyList.zip = LazyList.map₂ Prod.mk

def LazyList.join {α : Type u} :

LazyList (LazyList α) → LazyList α

The monadic join operation for lazy lists.

Equations

LazyList.join LazyList.nil = LazyList.nil
LazyList.join (LazyList.cons h t) = LazyList.append h { fn := fun x => LazyList.join (Thunk.get t) }

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

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

Equations

LazyList.for l f = LazyList.map f l

def LazyList.approx {α : Type u} :

Nat → LazyList α → List α

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

Equations

LazyList.approx 0 x = []
LazyList.approx x LazyList.nil = []
LazyList.approx (Nat.succ a) (LazyList.cons h t) = h :: LazyList.approx a (Thunk.get t)

def LazyList.filter {α : Type u} (p : α → Prop) [inst : DecidablePred p] :

LazyList α → LazyList α

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

LazyList.filter p LazyList.nil = LazyList.nil
LazyList.filter p (LazyList.cons h t) = if p h then LazyList.cons h { fn := fun x => LazyList.filter p (Thunk.get t) } else LazyList.filter p (Thunk.get t)

def LazyList.nth {α : Type u} :

LazyList α → Nat → Option α

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

Equations

LazyList.nth LazyList.nil x = none
LazyList.nth (LazyList.cons a tl) 0 = some a
LazyList.nth (LazyList.cons hd l) (Nat.succ n) = LazyList.nth (Thunk.get l) n

unsafe def LazyList.iterates {α : Type u} (f : α → α) :

α → LazyList α

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.

Equations

LazyList.iterates f x = let x := x; LazyList.cons x { fn := fun x_1 => LazyList.iterates f (f x) }

unsafe def LazyList.iota (i : Nat) :

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

Equations

LazyList.iota i = LazyList.iterates Nat.succ i