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.
- lazy_list.decidable_eq (lazy_list.cons x xs) (lazy_list.cons y ys) = dite (x = y) (λ (h : x = y), lazy_list.decidable_eq._match_1 x xs y ys h (lazy_list.decidable_eq (xs ()) (ys ()))) (λ (h : ¬x = y), is_false _)
- lazy_list.decidable_eq (lazy_list.cons _x _x_1) lazy_list.nil = is_false _
- lazy_list.decidable_eq lazy_list.nil (lazy_list.cons _x _x_1) = is_false _
- lazy_list.decidable_eq lazy_list.nil lazy_list.nil = is_true lazy_list.decidable_eq._main._proof_1
- lazy_list.decidable_eq._match_1 x xs y ys h (is_true h2) = have this : xs = ys, from _, is_true _
- lazy_list.decidable_eq._match_1 x xs y ys h (is_false h2) = is_false _
Traversal of lazy lists using an applicative effect.
init xs, if
xs non-empty, drops the last element of the list.
Otherwise, return the empty list.
interleave xs ys creates a list where elements of
interleave_all (xs::ys::zs::xss) creates a list where elements of
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.
Reverse the order of a
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.
Try applying function
f to every element of a
return the result of the first attempt that succeeds.
map for partial functions #
Partial map. If
f : Π a, p a → β is a partial function defined on
a : α satisfying
pmap f l h is essentially the same as
map f l
but is defined only when all members of
p, using the proof