Documentation

Mathlib.Data.LazyList.Basic

Definitions on lazy lists #

This file contains various definitions and proofs on lazy lists.

TODO: move the LazyList.lean file from core to mathlib.

theorem Thunk.ext {α : Type u} {a : Thunk α} {b : Thunk α} (eq : Thunk.get a = Thunk.get b) :
a = b
instance Thunk.instDecidableEqThunk {α : Type u} [inst : DecidableEq α] :
Equations

Isomorphism between strict and lazy lists.

Equations
  • One or more equations did not get rendered due to their size.
instance LazyList.decidableEq {α : Type u} [inst : DecidableEq α] :
Equations
def LazyList.traverse {m : Type u → Type u} [inst : Applicative m] {α : Type u} {β : Type u} (f : αm β) :
LazyList αm (LazyList β)

Traversal of lazy lists using an applicative effect.

Equations
Equations
  • One or more equations did not get rendered due to their size.
def LazyList.init {α : Type u_1} :
LazyList αLazyList α

init xs, if xs non-empty, drops the last element of the list. Otherwise, return the empty list.

Equations
def LazyList.find {α : Type u_1} (p : αProp) [inst : DecidablePred p] :
LazyList αOption α

Return the first object contained in the list that satisfies predicate p

Equations
def LazyList.interleave {α : Type u_1} :
LazyList αLazyList αLazyList α

interleave xs ys creates a list where elements of xs and ys alternate.

Equations
def LazyList.interleaveAll {α : Type u_1} :
List (LazyList α)LazyList α

interleaveAll (xs::ys::zs::xss) creates a list where elements of xs, ys and zs and the rest alternate. Every other element of the resulting list is taken from xs, every fourth is taken from ys, every eighth is taken from zs and so on.

Equations
def LazyList.bind {α : Type u_1} {β : Type u_2} :
LazyList α(αLazyList β) → LazyList β

Monadic bind operation for LazyList.

Equations
def LazyList.reverse {α : Type u_1} (xs : LazyList α) :

Reverse the order of a LazyList. It is done by converting to a List first because reversal involves evaluating all the list and if the list is all evaluated, List is a better representation for it than a series of thunks.

Equations
theorem LazyList.append_nil {α : Type u_1} (xs : LazyList α) :
LazyList.append xs (Thunk.pure LazyList.nil) = xs
theorem LazyList.append_assoc {α : Type u_1} (xs : LazyList α) (ys : LazyList α) (zs : LazyList α) :
LazyList.append (LazyList.append xs { fn := fun x => ys }) { fn := fun x => zs } = LazyList.append xs { fn := fun x => LazyList.append ys { fn := fun x => zs } }
theorem LazyList.append_bind {α : Type u_1} {β : Type u_2} (xs : LazyList α) (ys : Thunk (LazyList α)) (f : αLazyList β) :
def LazyList.mfirst {m : Type u_1 → Type u_2} [inst : Alternative m] {α : Type u_3} {β : Type u_1} (f : αm β) :
LazyList αm β

Try applying function f to every element of a LazyList and return the result of the first attempt that succeeds.

Equations
def LazyList.Mem {α : Type u_1} (x : α) :
LazyList αProp

Membership in lazy lists

Equations
Equations
  • LazyList.instMembershipLazyList = { mem := LazyList.Mem }
instance LazyList.Mem.decidable {α : Type u_1} [inst : DecidableEq α] (x : α) (xs : LazyList α) :
Decidable (x xs)
Equations
@[simp]
theorem LazyList.mem_nil {α : Type u_1} (x : α) :
x LazyList.nil False
@[simp]
theorem LazyList.mem_cons {α : Type u_1} (x : α) (y : α) (ys : Thunk (LazyList α)) :
theorem LazyList.forall_mem_cons {α : Type u_1} {p : αProp} {a : α} {l : Thunk (LazyList α)} :
((x : α) → x LazyList.cons a lp x) p a ((x : α) → x Thunk.get lp x)

map for partial functions #

def LazyList.pmap {α : Type u_1} {β : Type u_2} {p : αProp} (f : (a : α) → p aβ) (l : LazyList α) :
((a : α) → a lp a) → LazyList β

Partial map. If f : ∀ a, p a → β∀ a, p a → β→ β is a partial function defined on a : α satisfying p, then pmap f l h is essentially the same as map f l but is defined only when all members of l satisfy p, using the proof to apply f.

Equations
  • One or more equations did not get rendered due to their size.
  • LazyList.pmap f LazyList.nil x_2 = LazyList.nil
def LazyList.attach {α : Type u_1} (l : LazyList α) :
LazyList { x // x l }

"Attach" the proof that the elements of l are in l to produce a new LazyList with the same elements but in the type {x // x ∈ l}∈ l}.

Equations
instance LazyList.instReprLazyList {α : Type u_1} [inst : Repr α] :
Equations