# Functions for splitting monadic lazy lists. #

## Deprecation #

This material has been moved out of Mathlib to https://github.com/semorrison/lean-monadic-list.

Extract the prefix of a lazy list consisting of elements up to and including
the first element satisfying a monadic predicate.
Return (in the monad) the prefix as a `List`

, along with the remaining elements as a `MLList`

.

Extract the prefix of a lazy list consisting of elements up to and including
the first element satisfying a predicate.
Return (in the monad) the prefix as a `List`

, along with the remaining elements as a `MLList`

.

## Instances For

Extract a maximal prefix of a lazy list consisting of elements
satisfying a monadic predicate.
Return (in the monad) the prefix as a `List`

, along with the remaining elements as a `MLList`

.

(Note that the first element *not* satisfying the predicate will be generated,
and pushed back on to the remaining lazy list.)

Extract a maximal prefix of a lazy list consisting of elements
satisfying a predicate.
Return (in the monad) the prefix as a `List`

, along with the remaining elements as a `MLList`

.

(Note that the first element *not* satisfying the predicate will be generated,
and pushed back on to the remaining lazy list.)

## Instances For

Splits a lazy list into contiguous sublists of elements with the same value under a monadic function. Return a lazy lists of pairs, consisting of a value under that function, and a maximal list of elements having that value.

Splits a lazy list into contiguous sublists of elements with the same value under a function. Return a lazy lists of pairs, consisting of a value under that function, and a maximal list of elements having that value.

## Instances For

Split a lazy list into contiguous sublists,
starting a new sublist each time a monadic predicate changes from `false`

to `true`

.

## Equations

- L.splitAtBecomesTrueM p = MLList.splitAtBecomesTrueM.aux (L.groupByM p)