## Definitions on lazy lists #

This file contains various definitions and proofs on lazy lists.

TODO: move the `LazyList.lean`

file from core to mathlib.

## Equations

- One or more equations did not get rendered due to their size.
- LazyList.decidableEq LazyList.nil LazyList.nil = isTrue (_ : LazyList.nil = LazyList.nil)
- LazyList.decidableEq LazyList.nil (LazyList.cons hd tl) = isFalse (_ : ¬LazyList.nil = LazyList.cons hd tl)
- LazyList.decidableEq (LazyList.cons hd tl) LazyList.nil = isFalse (_ : ¬LazyList.cons hd tl = LazyList.nil)

Traversal of lazy lists using an applicative effect.

## Equations

- LazyList.traverse f LazyList.nil = pure LazyList.nil
- LazyList.traverse f (LazyList.cons x_1 xs) = Seq.seq (LazyList.cons <$> f x_1) fun x => Thunk.pure <$> LazyList.traverse f (Thunk.get xs)

## Equations

- One or more equations did not get rendered due to their size.

`init xs`

, if `xs`

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

## Equations

- LazyList.init LazyList.nil = LazyList.nil
- LazyList.init (LazyList.cons x_1 xs) = match Thunk.get xs with | LazyList.nil => LazyList.nil | LazyList.cons hd tl => LazyList.cons x_1 { fn := fun x => LazyList.init (Thunk.get xs) }

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

## Equations

- LazyList.find p LazyList.nil = none
- LazyList.find p (LazyList.cons x_1 xs) = if p x_1 then some x_1 else LazyList.find p (Thunk.get xs)

`interleave xs ys`

creates a list where elements of `xs`

and `ys`

alternate.

## Equations

- LazyList.interleave LazyList.nil x = x
- LazyList.interleave (LazyList.cons hd tl) LazyList.nil = LazyList.cons hd tl
- LazyList.interleave (LazyList.cons x_2 xs) (LazyList.cons y ys) = LazyList.cons x_2 { fn := fun x => LazyList.cons y { fn := fun x => LazyList.interleave (Thunk.get xs) (Thunk.get ys) } }

`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) = LazyList.interleave x_1 (LazyList.interleaveAll xs)

Monadic bind operation for `LazyList`

.

## Equations

- LazyList.bind LazyList.nil x = LazyList.nil
- LazyList.bind (LazyList.cons x_2 xs) x = LazyList.append (x x_2) { fn := fun x => LazyList.bind (Thunk.get xs) x }

## Equations

- LazyList.instMonadLazyList = Monad.mk

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 x_1 xs) = HOrElse.hOrElse (f x_1) fun x => LazyList.mfirst f (Thunk.get xs)

Membership in lazy lists

## Equations

- LazyList.Mem x LazyList.nil = False
- LazyList.Mem x (LazyList.cons x_2 xs) = (x = x_2 ∨ LazyList.Mem x (Thunk.get xs))

## Equations

- LazyList.instMembershipLazyList = { mem := LazyList.Mem }

## Equations

- One or more equations did not get rendered due to their size.
- LazyList.Mem.decidable x LazyList.nil = isFalse (_ : ¬LazyList.Mem x LazyList.nil)

### map for partial functions #

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

"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

- LazyList.attach l = LazyList.pmap Subtype.mk l (_ : ∀ (x : α), x ∈ l → x ∈ l)

## Equations

- LazyList.instReprLazyList = { reprPrec := fun xs x => repr (LazyList.toList xs) }