Documentation

Mathlib.Data.MLList.Split

Functions for splitting monadic lazy lists. #

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.

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 }
Instances For
    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.)

    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 }
    Instances For
      partial def MLList.groupByM {α : Type u} {β : 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.

      def MLList.groupBy {α : Type u} {β : 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)
      Instances For
        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
        Instances For
          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 α)
          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 }
          Instances For