mathlib3 documentation

data.lazy_list.basic

Definitions on lazy lists #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file contains various definitions and proofs on lazy lists.

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

source
def thunk.mk {α : Type u_1} (x : α) :
thunk α

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

Equations
source
@[protected, instance]
def thunk.decidable_eq {α : Type u} [decidable_eq α] :
decidable_eq (thunk α)
Equations
source
def lazy_list.list_equiv_lazy_list (α : Type u_1) :
list α ≃ lazy_list α

Isomorphism between strict and lazy lists.

Equations
source
@[protected, instance]
def lazy_list.decidable_eq {α : Type u} [decidable_eq α] :
decidable_eq (lazy_list α)
Equations
source
@[protected]
def lazy_list.traverse {m : Type u → Type u} [applicative m] {α β : Type u} (f : α → m β) :
lazy_list α → m (lazy_list β)

Traversal of lazy lists using an applicative effect.

Equations
source
@[protected, instance]
def lazy_list.traversable  :
traversable lazy_list
Equations
source
@[protected, instance]
def lazy_list.is_lawful_traversable  :
is_lawful_traversable lazy_list
Equations
source
def lazy_list.init {α : Type u_1} :
lazy_list α → lazy_list α

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

Equations
source
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
source
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
source
def lazy_list.interleave_all {α : Type u_1} :
list (lazy_list α) → lazy_list α

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
source
@[protected]
def lazy_list.bind {α : Type u_1} {β : Type u_2} :
lazy_list α → (α → lazy_list β) → lazy_list β

Monadic bind operation for lazy_list.

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

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
source
@[protected, instance]
def lazy_list.monad  :
monad lazy_list
Equations
source
theorem lazy_list.append_nil {α : Type u_1} (xs : lazy_list α) :
xs.append (λ («_» : unit), lazy_list.nil) = xs
source
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))
source
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 unit.star()).bind f)
source
@[protected, instance]
def lazy_list.is_lawful_monad  :
is_lawful_monad lazy_list
source
def lazy_list.mfirst {m : Type u_1 → Type u_2} [alternative m] {α : Type u_3} {β : Type u_1} (f : α → 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
source
@[protected]
def lazy_list.mem {α : Type u_1} (x : α) :
lazy_list α → Prop

Membership in lazy lists

Equations
source
@[protected, instance]
def lazy_list.has_mem {α : out_param (Type u_1)} :
has_mem α (lazy_list α)
Equations
source
@[protected, instance]
def lazy_list.mem.decidable {α : Type u_1} [decidable_eq α] (x : α) (xs : lazy_list α) :
decidable (x ∈ xs)
Equations
source
@[simp]
theorem lazy_list.mem_nil {α : Type u_1} (x : α) :
x ∈ lazy_list.nil ↔ false
source
@[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 unit.star()
source
theorem lazy_list.forall_mem_cons {α : Type u_1} {p : α → Prop} {a : α} {l : thunk (lazy_list α)} :
(∀ (x : α), x ∈ lazy_list.cons a l → p x) ↔ p a ∧ ∀ (x : α), x ∈ l unit.star() → p x

map for partial functions #

source
@[simp]
def lazy_list.pmap {α : Type u_1} {β : Type u_2} {p : α → Prop} (f : Π (a : α), p a → β) (l : lazy_list α) :
(∀ (a : α), a ∈ l → p 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
source
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
source
@[protected, instance]
def lazy_list.has_repr {α : Type u_1} [has_repr α] :
has_repr (lazy_list α)
Equations