Documentation

Std.Data.Iterators.Consumers.Loop

Loop consumers #

This module provides consumers that iterate over a given iterator, applying a certain user-supplied function in every iteration. Concretely, the following operations are provided:

These operations are implemented using the IteratorLoop and IteratorLoopPartial typeclasses.

instance Std.Iterators.instForInIterOfMonadOfFiniteOfIteratorLoopId (α β : Type w) (n : Type w → Type w') [Monad n] [Iterator α Id β] [Finite α Id] [IteratorLoop α Id n] :
ForIn n (Iter β) β
Equations
    instance Std.Iterators.instForMIterOfFiniteOfIteratorLoopId {m : Type w → Type w'} {α β : Type w} [Iterator α Id β] [Finite α Id] [IteratorLoop α Id m] :
    ForM m (Iter β) β
    Equations
      @[inline]
      def Std.Iterators.Iter.foldM {m : Type w → Type w'} [Monad m] {α β γ : Type w} [Iterator α Id β] [Finite α Id] [IteratorLoop α Id m] (f : γβm γ) (init : γ) (it : Iter β) :
      m γ

      Folds a monadic function over an iterator from the left, accumulating a value starting with init. The accumulated value is combined with the each element of the list in order, using f.

      It is equivalent to it.toList.foldlM.

      This function requires a Finite instance proving that the iterator will finish after a finite number of steps. If the iterator is not finite or such an instance is not available, consider using it.allowNontermination.foldM instead of it.foldM. However, it is not possible to formally verify the behavior of the partial variant.

      Equations
        Instances For
          @[inline]
          def Std.Iterators.Iter.Partial.foldM {m : Type w → Type w'} [Monad m] {α β γ : Type w} [Iterator α Id β] [IteratorLoopPartial α Id m] (f : γβm γ) (init : γ) (it : Partial β) :
          m γ

          Folds a monadic function over an iterator from the left, accumulating a value starting with init. The accumulated value is combined with the each element of the list in order, using f.

          It is equivalent to it.toList.foldlM.

          This is a partial, potentially nonterminating, function. It is not possible to formally verify its behavior. If the iterator has a Finite instance, consider using IterM.foldM instead.

          Equations
            Instances For
              @[inline]
              def Std.Iterators.Iter.fold {α β γ : Type w} [Iterator α Id β] [Finite α Id] [IteratorLoop α Id Id] (f : γβγ) (init : γ) (it : Iter β) :
              γ

              Folds a function over an iterator from the left, accumulating a value starting with init. The accumulated value is combined with the each element of the list in order, using f.

              It is equivalent to it.toList.foldl.

              This function requires a Finite instance proving that the iterator will finish after a finite number of steps. If the iterator is not finite or such an instance is not available, consider using it.allowNontermination.fold instead of it.fold. However, it is not possible to formally verify the behavior of the partial variant.

              Equations
                Instances For
                  @[inline]
                  def Std.Iterators.Iter.Partial.fold {α β γ : Type w} [Iterator α Id β] [IteratorLoopPartial α Id Id] (f : γβγ) (init : γ) (it : Partial β) :
                  γ

                  Folds a function over an iterator from the left, accumulating a value starting with init. The accumulated value is combined with the each element of the list in order, using f.

                  It is equivalent to it.toList.foldl.

                  This is a partial, potentially nonterminating, function. It is not possible to formally verify its behavior. If the iterator has a Finite instance, consider using IterM.fold instead.

                  Equations
                    Instances For