Functions for splitting monadic lazy lists.

Deprecation

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

@[deprecated]

partial def MLList.getUpToFirstM {α : Type u} {m : Type u → Type u} [Monad m] (L : MLList m α) (p : α → m (ULift.{u, 0} Bool)) : m (List α × MLList m α)

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.

@[deprecated]

def MLList.getUpToFirst {α : Type u} {m : Type u → Type u} [Monad m] (L : MLList m α) (p : α → Bool) : m (List α × MLList m α)

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.

Equations

• L.getUpToFirst p = L.getUpToFirstM fun (a : α) => pure { down := p a }

@[deprecated]

partial def MLList.splitWhileM {α : Type u} {m : Type u → Type u} [Monad m] (L : MLList m α) (p : α → m (ULift.{u, 0} Bool)) : m (List α × MLList m α)

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.)

@[deprecated]

def MLList.splitWhile {α : Type u} {m : Type u → Type u} [Monad m] (L : MLList m α) (p : α → Bool) : m (List α × MLList m α)

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.)

Equations

• L.splitWhile p = L.splitWhileM fun (a : α) => pure { down := p a }

@[deprecated]

partial def MLList.groupByM {α β : Type u} {m : Type u → Type u} [Monad m] [DecidableEq β] (L : MLList m α) (f : α → m β) : MLList m (β × List α)

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.

@[deprecated]

def MLList.groupBy {α β : Type u} {m : Type u → Type u} [Monad m] [DecidableEq β] (L : MLList m α) (f : α → β) : MLList m (β × List α)

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.

Equations

• L.groupBy f = L.groupByM fun (a : α) => pure (f a)

@[deprecated]

def MLList.splitAtBecomesTrueM {α : Type u} {m : Type u → Type u} [Monad m] (L : MLList m α) (p : α → m (ULift.{u, 0} Bool)) : MLList m (List α)

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)

partial def MLList.splitAtBecomesTrueM.aux {α : Type u} {m : Type u → Type u} [Monad m] (M : MLList m (ULift.{u, 0} Bool × List α)) : MLList m (List α)

@[deprecated]

def MLList.splitAtBecomesTrue {α : Type u} {m : Type u → Type u} [Monad m] (L : MLList m α) (p : α → Bool) : MLList m (List α)

Split a lazy list into contiguous sublists, starting a new sublist each time a predicate changes from false to true.

Equations

• L.splitAtBecomesTrue p = L.splitAtBecomesTrueM fun (a : α) => pure { down := p a }