mathlib documentation

data.lazy_list.basic

Definitions on lazy lists

This file contains various definitions and proofs on lazy lists.

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

def thunk.mk {α : Type u_1} :
α → thunk α

Creates a thunk with a (non-lazy) constant value.

Equations
@[instance]
def thunk.decidable_eq {α : Type u} [decidable_eq α] :

Equations
def lazy_list.list_equiv_lazy_list (α : Type u_1) :

Isomorphism between strict and lazy lists.

Equations
@[instance]
def lazy_list.inhabited {α : Type u} :

Equations
@[instance]

Equations
def lazy_list.traverse {m : Type uType u} [applicative m] {α β : Type u} :
(α → m β)lazy_list αm (lazy_list β)

Traversal of lazy lists using an applicative effect.

Equations
@[instance]

Equations
def lazy_list.init {α : Type u_1} :

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

Equations
def lazy_list.find {α : Type u_1} (p : α → Prop) [decidable_pred p] :
lazy_list αoption α

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

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

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

Equations
def lazy_list.interleave_all {α : Type u_1} :

interleave_all (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 lazy_list.bind {α : Type u_1} {β : Type u_2} :
lazy_list α(α → lazy_list β)lazy_list β

Monadic bind operation for lazy_list.

Equations
def lazy_list.reverse {α : Type u_1} :

Reverse the order of a lazy_list. 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 lazy_list.append_nil {α : Type u_1} (xs : lazy_list α) :
xs.append (λ («_» : unit), lazy_list.nil) = xs

theorem lazy_list.append_assoc {α : Type u_1} (xs ys zs : lazy_list α) :
(xs.append (λ («_» : unit), ys)).append (λ («_» : unit), zs) = xs.append (λ («_» : unit), ys.append (λ («_» : unit), zs))

theorem lazy_list.append_bind {α : Type u_1} {β : Type u_2} (xs : lazy_list α) (ys : thunk (lazy_list α)) (f : α → lazy_list β) :
(xs.append ys).bind f = (xs.bind f).append (λ («_» : unit), (ys ()).bind f)

def lazy_list.mfirst {m : Type u_1Type u_2} [alternative m] {α : Type u_3} {β : Type u_1} :
(α → m β)lazy_list αm β

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

Equations
def lazy_list.mem {α : Type u_1} :
α → lazy_list α → Prop

Membership in lazy lists

Equations
@[instance]
def lazy_list.has_mem {α : out_param (Type u_1)} :

Equations
@[instance]
def lazy_list.mem.decidable {α : Type u_1} [decidable_eq α] (x : α) (xs : lazy_list α) :
decidable (x xs)

Equations
@[simp]
theorem lazy_list.mem_nil {α : Type u_1} (x : α) :

@[simp]
theorem lazy_list.mem_cons {α : Type u_1} (x y : α) (ys : thunk (lazy_list α)) :
x lazy_list.cons y ys x = y x ys ()

theorem lazy_list.forall_mem_cons {α : Type u_1} {p : α → Prop} {a : α} {l : thunk (lazy_list α)} :
(∀ (x : α), x lazy_list.cons a lp x) p a ∀ (x : α), x l ()p x

map for partial functions

@[simp]
def lazy_list.pmap {α : Type u_1} {β : Type u_2} {p : α → Prop} (f : Π (a : α), p a → β) (l : lazy_list α) :
(∀ (a : α), a lp a)lazy_list β

Partial map. If f : Π 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
def lazy_list.attach {α : Type u_1} (l : lazy_list α) :
lazy_list {x // x l}

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

Equations
@[instance]
def lazy_list.has_repr {α : Type u_1} [has_repr α] :

Equations