Lazy lists #
Deprecated. This module is deprecated and will be removed in the future.
Most use cases can use MLList
. Without custom support from the kernel
(previously provided in Lean 3) this type is not very useful,
but was ported from Lean 3 anyway.
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 α
.)
The singleton lazy list.
Equations
- LazyList.singleton x = LazyList.cons x (Thunk.pure LazyList.nil)
Instances For
Constructs a lazy list from a list.
Equations
- LazyList.ofList [] = LazyList.nil
- LazyList.ofList (h :: t) = LazyList.cons h { fn := fun (x : Unit) => LazyList.ofList t }
Instances For
Converts a lazy list to a list. If the lazy list is infinite, then this function does not terminate.
Equations
- LazyList.nil.toList = []
- (LazyList.cons h t).toList = h :: t.get.toList
Instances For
Returns the first element of the lazy list,
or default
if the lazy list is empty.
Equations
- LazyList.nil.headI = default
- (LazyList.cons h t).headI = h
Instances For
Removes the first element of the lazy list.
Equations
- LazyList.nil.tail = LazyList.nil
- (LazyList.cons h t).tail = t.get
Instances For
Appends two lazy lists.
Equations
- LazyList.nil.append x = x.get
- (LazyList.cons h t).append x = LazyList.cons h { fn := fun (x_1 : Unit) => t.get.append x }
Instances For
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 : Unit) => LazyList.map f t.get }
Instances For
Maps a binary function over two lazy list.
Like LazyList.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 : Unit) => LazyList.map₂ f t₁.get t₂.get }
Instances For
The monadic join operation for lazy lists.
Equations
- LazyList.nil.join = LazyList.nil
- (LazyList.cons h t).join = h.append { fn := fun (x : Unit) => t.get.join }
Instances For
The list containing the first n
elements of a lazy list.
Equations
- LazyList.take 0 x = []
- LazyList.take x LazyList.nil = []
- LazyList.take a.succ (LazyList.cons h t) = h :: LazyList.take a t.get
Instances For
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 : Unit) => LazyList.filter p t.get } else LazyList.filter p t.get
Instances For
The nth element of a lazy list as an option (like List.get?
).
Equations
- LazyList.nil.get? x = none
- (LazyList.cons a tl).get? 0 = some a
- (LazyList.cons hd l).get? n.succ = l.get.get? n
Instances For
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.
The infinite lazy list [i, i+1, i+2, ...]
Equations
Instances For
Equations
- LazyList.nil.decidableEq LazyList.nil = isTrue ⋯
- (LazyList.cons x_2 xs).decidableEq (LazyList.cons y ys) = if h : x_2 = y then match xs.get.decidableEq ys.get with | isFalse h2 => isFalse ⋯ | isTrue h2 => isTrue ⋯ else isFalse ⋯
- LazyList.nil.decidableEq (LazyList.cons hd tl) = isFalse ⋯
- (LazyList.cons hd tl).decidableEq LazyList.nil = isFalse ⋯
Traversal of lazy lists using an applicative effect.
Equations
- LazyList.traverse f LazyList.nil = pure LazyList.nil
- LazyList.traverse f (LazyList.cons h t) = Seq.seq (LazyList.cons <$> f h) fun (x : Unit) => Thunk.pure <$> LazyList.traverse f t.get
Instances For
init xs
, if xs
non-empty, drops the last element of the list.
Otherwise, return the empty list.
Equations
- LazyList.nil.init = LazyList.nil
- (LazyList.cons h t).init = match t.get with | LazyList.nil => LazyList.nil | LazyList.cons hd tl => LazyList.cons h { fn := fun (x : Unit) => t.get.init }
Instances For
Return the first object contained in the list that satisfies
predicate p
Equations
- LazyList.find p LazyList.nil = none
- LazyList.find p (LazyList.cons h t) = if p h then some h else LazyList.find p t.get
Instances For
interleave xs ys
creates a list where elements of xs
and ys
alternate.
Equations
- LazyList.nil.interleave x = x
- (LazyList.cons hd tl).interleave LazyList.nil = LazyList.cons hd tl
- (LazyList.cons x_2 xs).interleave (LazyList.cons y ys) = LazyList.cons x_2 { fn := fun (x : Unit) => LazyList.cons y { fn := fun (x : Unit) => xs.get.interleave ys.get } }
Instances For
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
- LazyList.interleaveAll [] = LazyList.nil
- LazyList.interleaveAll (x_1 :: xs) = x_1.interleave (LazyList.interleaveAll xs)
Instances For
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
- xs.reverse = LazyList.ofList xs.toList.reverse
Instances For
Try applying function f
to every element of a LazyList
and
return the result of the first attempt that succeeds.
Equations
- LazyList.mfirst f LazyList.nil = failure
- LazyList.mfirst f (LazyList.cons h t) = HOrElse.hOrElse (f h) fun (x : Unit) => LazyList.mfirst f t.get
Instances For
Membership in lazy lists
Equations
- LazyList.Mem x LazyList.nil = False
- LazyList.Mem x (LazyList.cons h t) = (x = h ∨ LazyList.Mem x t.get)
Instances For
Equations
- LazyList.instMembership = { mem := fun (l : LazyList α) (a : α) => LazyList.Mem a l }
Equations
- One or more equations did not get rendered due to their size.
- LazyList.Mem.decidable x LazyList.nil = isFalse ⋯
map for partial functions #
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
- LazyList.pmap f LazyList.nil x_2 = LazyList.nil
- LazyList.pmap f (LazyList.cons x_2 xs) H = LazyList.cons (f x_2 ⋯) { fn := fun (x : Unit) => LazyList.pmap f xs.get ⋯ }
Instances For
"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}
.
Equations
- l.attach = LazyList.pmap Subtype.mk l ⋯