The Lean Language Reference

21.3. Consuming Iterators

There are three primary ways to consume an iterator:

Converting it to a sequential data structure

The functions Iter.toList, Iter.toArray, and their monadic equivalents IterM.toList and IterM.toArray, construct a lists or arrays that contain the values from the iterator, in order. Only finite iterators can be converted to sequential data structures.

Lean.Parser.Term.doFor : doElem`for x in e do s` iterates over `e` assuming `e`'s type has an instance of the `ForIn` typeclass. `break` and `continue` are supported inside `for` loops. `for x in e, x2 in e2, ... do s` iterates of the given collections in parallel, until at least one of them is exhausted. The types of `e2` etc. must implement the `Std.ToStream` typeclass. for loops

A Lean.Parser.Term.doFor : doElem`for x in e do s` iterates over `e` assuming `e`'s type has an instance of the `ForIn` typeclass. `break` and `continue` are supported inside `for` loops. `for x in e, x2 in e2, ... do s` iterates of the given collections in parallel, until at least one of them is exhausted. The types of `e2` etc. must implement the `Std.ToStream` typeclass. for loop can consume an iterator, making each value available in its body. This requires that the iterator have either an instance of IteratorLoop or IteratorLoopPartial for the loop's monad.

Stepping through iterators

Iterators can provide their values one-by-one, with client code explicitly requesting each new value in turn. When stepped through, iterators perform only enough computation to yield the requested value.

Converting Iterators to Lists

In countdown, an iterator over a range is transformed into an iterator over strings using Iter.map. This call to Iter.map does not result in any iteration over the range until Iter.toList is called, at which point each element of the range is produced and transformed into a string.

def countdown : String := let steps : Iter String := (0...10).iter.map (s!"{10 - ·}!\n") String.join steps.toList 10! 9! 8! 7! 6! 5! 4! 3! 2! 1! #eval IO.println countdown 
10!
9!
8!
7!
6!
5!
4!
3!
2!
1!
Live ↪
Converting Infinite Iterators to Lists

Attempting to construct a list of all the natural numbers from an iterator fails:

def allNats : List Nat := let steps : Iter Nat := (0...*).iter failed to synthesize instance of type class Finite (Std.Rxi.Iterator Nat) Id Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.steps.toList

The resulting error message states that there is no Finite instance:

failed to synthesize instance of type class
  Finite (Std.Rxi.Iterator Nat) Id

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.

If the failure to synthesize the instance is due to a missing proof, or if an infinite loop is desirable for an application, then the fact that consuming the iterator may not terminate can be hidden using Iter.allowNontermination:

def allNats : List Nat := let steps : Iter Nat := (0...*).iter steps.allowNontermination.toList
Live ↪
Consuming Iterators in Loops

This program creates an iterator of strings from a range, and then consumes the strings in a Lean.Parser.Term.doFor : doElem`for x in e do s` iterates over `e` assuming `e`'s type has an instance of the `ForIn` typeclass. `break` and `continue` are supported inside `for` loops. `for x in e, x2 in e2, ... do s` iterates of the given collections in parallel, until at least one of them is exhausted. The types of `e2` etc. must implement the `Std.ToStream` typeclass. for loop:

def countdown (n : Nat) : IO Unit := do let steps : Iter String := (0...n).iter.map (s!"{n - ·}!") for i in steps do IO.println i IO.println "Blastoff!" 5! 4! 3! 2! 1! Blastoff! #eval countdown 5 
5!
4!
3!
2!
1!
Blastoff!
Live ↪
Consuming Iterators Directly

The function countdown calls the range iterator's step function directly, handling each of the three possible cases.

def countdown (n : Nat) : IO Unit := do let steps : Iter Nat := (0...n).iter go steps where go iter := do match iter.step with | .done _ => pure () | .skip iter' _ => go iter' | .yield iter' i _ => do IO.println s!"{i}!" if i == 2 then IO.println s!"Almost there..." go iter' termination_by iter.finitelyManySteps
Live ↪

21.3.1. Stepping Iterators

Iterators are manually stepped using Iter.step or IterM.step.

🔗def
Std.Iterators.Iter.step.{w} {α β : Type w} [Iterator α Id β]
  (it : Iter β) : it.Step
Std.Iterators.Iter.step.{w} {α β : Type w}
  [Iterator α Id β] (it : Iter β) :
  it.Step

Makes a single step with the given iterator it, potentially emitting a value and providing a succeeding iterator. If this function is used recursively, termination can sometimes be proved with the termination measures it.finitelyManySteps and it.finitelyManySkips.

🔗def
Std.Iterators.IterM.step.{w, w'} {α : Type w} {m : Type w → Type w'}
  {β : Type w} [Iterator α m β] (it : IterM m β) :
  m (Std.Shrink it.Step)
Std.Iterators.IterM.step.{w, w'}
  {α : Type w} {m : Type w → Type w'}
  {β : Type w} [Iterator α m β]
  (it : IterM m β) :
  m (Std.Shrink it.Step)

Makes a single step with the given iterator it, potentially emitting a value and providing a succeeding iterator. If this function is used recursively, termination can sometimes be proved with the termination measures it.finitelyManySteps and it.finitelyManySkips.

21.3.1.1. Termination

When manually stepping an finite iterator, the termination measures finitelyManySteps and finitelyManySkips can be used to express that each step brings iteration closer to the end. The proof automation for well-founded recursion is pre-configured to prove that recursive calls after steps reduce these measures.

Finitely Many Skips

This function returns the first element of an iterator, if there is one, or none otherwise. Because the iterator must be productive, it is guaranteed to return an element after at most a finite number of skips. This function terminates even for infinite iterators.

def getFirst [Iterator α Id β] [Productive α Id] (it : @Iter α β) : Option β := match it.step with | .done .. => none | .skip it' .. => getFirst it' | .yield _ x .. => pure x termination_by it.finitelyManySkips
Live ↪
🔗def
Std.Iterators.Iter.finitelyManySteps.{w} {α β : Type w}
  [Iterator α Id β] [Finite α Id] (it : Iter β) :
  IterM.TerminationMeasures.Finite α Id
Std.Iterators.Iter.finitelyManySteps.{w}
  {α β : Type w} [Iterator α Id β]
  [Finite α Id] (it : Iter β) :
  IterM.TerminationMeasures.Finite α Id

Termination measure to be used in well-founded recursive functions recursing over a finite iterator (see also Finite).

🔗def
Std.Iterators.IterM.finitelyManySteps.{w, w'} {α : Type w}
  {m : Type w → Type w'} {β : Type w} [Iterator α m β] [Finite α m]
  (it : IterM m β) : IterM.TerminationMeasures.Finite α m
Std.Iterators.IterM.finitelyManySteps.{w,
    w'}
  {α : Type w} {m : Type w → Type w'}
  {β : Type w} [Iterator α m β]
  [Finite α m] (it : IterM m β) :
  IterM.TerminationMeasures.Finite α m

Termination measure to be used in well-founded recursive functions recursing over a finite iterator (see also Finite).

🔗structure
Std.Iterators.IterM.TerminationMeasures.Finite.{w, w'} (α : Type w)
  (m : Type w → Type w') {β : Type w} [Iterator α m β] : Type w
Std.Iterators.IterM.TerminationMeasures.Finite.{w,
    w'}
  (α : Type w) (m : Type w → Type w')
  {β : Type w} [Iterator α m β] : Type w

This type is a wrapper around IterM so that it becomes a useful termination measure for recursion over finite iterators. See also IterM.finitelyManySteps and Iter.finitelyManySteps.

Constructor

Std.Iterators.IterM.TerminationMeasures.Finite.mk.{w, w'}

Fields

it : IterM m β
🔗def
Std.Iterators.Iter.finitelyManySkips.{w} {α β : Type w}
  [Iterator α Id β] [Productive α Id] (it : Iter β) :
  IterM.TerminationMeasures.Productive α Id
Std.Iterators.Iter.finitelyManySkips.{w}
  {α β : Type w} [Iterator α Id β]
  [Productive α Id] (it : Iter β) :
  IterM.TerminationMeasures.Productive α
    Id

Termination measure to be used in well-founded recursive functions recursing over a productive iterator (see also Productive).

🔗def
Std.Iterators.IterM.finitelyManySkips.{w, w'} {α : Type w}
  {m : Type w → Type w'} {β : Type w} [Iterator α m β] [Productive α m]
  (it : IterM m β) : IterM.TerminationMeasures.Productive α m
Std.Iterators.IterM.finitelyManySkips.{w,
    w'}
  {α : Type w} {m : Type w → Type w'}
  {β : Type w} [Iterator α m β]
  [Productive α m] (it : IterM m β) :
  IterM.TerminationMeasures.Productive α m

Termination measure to be used in well-founded recursive functions recursing over a productive iterator (see also Productive).

🔗structure
Std.Iterators.IterM.TerminationMeasures.Productive.{w, w'} (α : Type w)
  (m : Type w → Type w') {β : Type w} [Iterator α m β] : Type w
Std.Iterators.IterM.TerminationMeasures.Productive.{w,
    w'}
  (α : Type w) (m : Type w → Type w')
  {β : Type w} [Iterator α m β] : Type w

This type is a wrapper around IterM so that it becomes a useful termination measure for recursion over productive iterators. See also IterM.finitelyManySkips and Iter.finitelyManySkips.

Constructor

Std.Iterators.IterM.TerminationMeasures.Productive.mk.{w, w'}

Fields

it : IterM m β

21.3.2. Consuming Pure Iterators

🔗def
Std.Iterators.Iter.fold.{w, x} {α β : Type w} {γ : Type x}
  [Iterator α Id β] [Finite α Id] [IteratorLoop α Id Id] (f : γ → β → γ)
  (init : γ) (it : Iter β) : γ
Std.Iterators.Iter.fold.{w, x}
  {α β : Type w} {γ : Type x}
  [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.

🔗def
Std.Iterators.Iter.foldM.{x, x', w} {m : Type x → Type x'} [Monad m]
  {α β : Type w} {γ : Type x} [Iterator α Id β] [Finite α Id]
  [IteratorLoop α Id m] (f : γ → β → m γ) (init : γ) (it : Iter β) : m γ
Std.Iterators.Iter.foldM.{x, x', w}
  {m : Type x → Type x'} [Monad m]
  {α β : Type w} {γ : Type x}
  [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.

🔗def
Std.Iterators.Iter.count.{w} {α β : Type w} [Iterator α Id β]
  [Finite α Id] [IteratorLoop α Id Id] (it : Iter β) : Nat
Std.Iterators.Iter.count.{w}
  {α β : Type w} [Iterator α Id β]
  [Finite α Id] [IteratorLoop α Id Id]
  (it : Iter β) : Nat

Steps through the whole iterator, counting the number of outputs emitted.

Performance:

This function's runtime is linear in the number of steps taken by the iterator.

🔗def
Std.Iterators.Iter.any.{w} {α β : Type w} [Iterator α Id β]
  [IteratorLoop α Id Id] [Finite α Id] (p : β → Bool) (it : Iter β) :
  Bool
Std.Iterators.Iter.any.{w} {α β : Type w}
  [Iterator α Id β] [IteratorLoop α Id Id]
  [Finite α Id] (p : β → Bool)
  (it : Iter β) : Bool

Returns true if the pure predicate p returns true for any element emitted by the iterator it.

O(|xs|). Short-circuits upon encountering the first match. The elements in it are examined in order of iteration.

🔗def
Std.Iterators.Iter.anyM.{w, w'} {α β : Type w} {m : Type → Type w'}
  [Monad m] [Iterator α Id β] [IteratorLoop α Id m] [Finite α Id]
  (p : β → m Bool) (it : Iter β) : m Bool
Std.Iterators.Iter.anyM.{w, w'}
  {α β : Type w} {m : Type → Type w'}
  [Monad m] [Iterator α Id β]
  [IteratorLoop α Id m] [Finite α Id]
  (p : β → m Bool) (it : Iter β) : m Bool

Returns true if the monadic predicate p returns true for any element emitted by the iterator it.

O(|xs|). Short-circuits upon encountering the first match. The elements in it are examined in order of iteration.

🔗def
Std.Iterators.Iter.all.{w} {α β : Type w} [Iterator α Id β]
  [IteratorLoop α Id Id] [Finite α Id] (p : β → Bool) (it : Iter β) :
  Bool
Std.Iterators.Iter.all.{w} {α β : Type w}
  [Iterator α Id β] [IteratorLoop α Id Id]
  [Finite α Id] (p : β → Bool)
  (it : Iter β) : Bool

Returns true if the pure predicate p returns true for all elements emitted by the iterator it.

O(|xs|). Short-circuits upon encountering the first mismatch. The elements in it are examined in order of iteration.

🔗def
Std.Iterators.Iter.allM.{w, w'} {α β : Type w} {m : Type → Type w'}
  [Monad m] [Iterator α Id β] [IteratorLoop α Id m] [Finite α Id]
  (p : β → m Bool) (it : Iter β) : m Bool
Std.Iterators.Iter.allM.{w, w'}
  {α β : Type w} {m : Type → Type w'}
  [Monad m] [Iterator α Id β]
  [IteratorLoop α Id m] [Finite α Id]
  (p : β → m Bool) (it : Iter β) : m Bool

Returns true if the monadic predicate p returns true for all elements emitted by the iterator it.

O(|xs|). Short-circuits upon encountering the first mismatch. The elements in it are examined in order of iteration.

🔗def
Std.Iterators.Iter.find?.{w} {α β : Type w} [Iterator α Id β]
  [IteratorLoop α Id Id] [Finite α Id] (it : Iter β) (f : β → Bool) :
  Option β
Std.Iterators.Iter.find?.{w}
  {α β : Type w} [Iterator α Id β]
  [IteratorLoop α Id Id] [Finite α Id]
  (it : Iter β) (f : β → Bool) : Option β

Steps through the iterator until an element satisfies f, at which point iteration stops and the element is returned. If no element satisfies f, then the result is none.

🔗def
Std.Iterators.Iter.findM?.{w, w'} {α β : Type w} {m : Type w → Type w'}
  [Monad m] [Iterator α Id β] [IteratorLoop α Id m] [Finite α Id]
  (it : Iter β) (f : β → m (ULift Bool)) : m (Option β)
Std.Iterators.Iter.findM?.{w, w'}
  {α β : Type w} {m : Type w → Type w'}
  [Monad m] [Iterator α Id β]
  [IteratorLoop α Id m] [Finite α Id]
  (it : Iter β) (f : β → m (ULift Bool)) :
  m (Option β)

Steps through the iterator until an element satisfies the monadic predicate f, at which point iteration stops and the element is returned. If no element satisfies f, then the result is none.

🔗def
Std.Iterators.Iter.findSome?.{w, x} {α β : Type w} {γ : Type x}
  [Iterator α Id β] [IteratorLoop α Id Id] [Finite α Id] (it : Iter β)
  (f : β → Option γ) : Option γ
Std.Iterators.Iter.findSome?.{w, x}
  {α β : Type w} {γ : Type x}
  [Iterator α Id β] [IteratorLoop α Id Id]
  [Finite α Id] (it : Iter β)
  (f : β → Option γ) : Option γ

Steps through the iterator until f returns some for an element, at which point iteration stops and the result of f is returned. If the iterator is completely consumed without f returning some, then the result is none.

🔗def
Std.Iterators.Iter.findSomeM?.{w, x, w'} {α β : Type w} {γ : Type x}
  {m : Type x → Type w'} [Monad m] [Iterator α Id β]
  [IteratorLoop α Id m] [Finite α Id] (it : Iter β)
  (f : β → m (Option γ)) : m (Option γ)
Std.Iterators.Iter.findSomeM?.{w, x, w'}
  {α β : Type w} {γ : Type x}
  {m : Type x → Type w'} [Monad m]
  [Iterator α Id β] [IteratorLoop α Id m]
  [Finite α Id] (it : Iter β)
  (f : β → m (Option γ)) : m (Option γ)

Steps through the iterator until the monadic function f returns some for an element, at which point iteration stops and the result of f is returned. If the iterator is completely consumed without f returning some, then the result is none.

🔗def
Std.Iterators.Iter.atIdx?.{u_1} {α β : Type u_1} [Iterator α Id β]
  [Productive α Id] [IteratorAccess α Id] (n : Nat) (it : Iter β) :
  Option β
Std.Iterators.Iter.atIdx?.{u_1}
  {α β : Type u_1} [Iterator α Id β]
  [Productive α Id] [IteratorAccess α Id]
  (n : Nat) (it : Iter β) : Option β

Returns the n-th value emitted by it, or none if it terminates earlier.

For monadic iterators, the monadic effects of this operation may differ from manually iterating to the n-th value because atIdx? can take shortcuts. By the signature, the return value is guaranteed to plausible in the sense of IterM.IsPlausibleNthOutputStep.

This function is only available for iterators that explicitly support it by implementing the IteratorAccess typeclass.

🔗def
Std.Iterators.Iter.atIdxSlow?.{u_1} {α β : Type u_1} [Iterator α Id β]
  [Productive α Id] (n : Nat) (it : Iter β) : Option β
Std.Iterators.Iter.atIdxSlow?.{u_1}
  {α β : Type u_1} [Iterator α Id β]
  [Productive α Id] (n : Nat)
  (it : Iter β) : Option β

If possible, takes n steps with the iterator it and returns the n-th emitted value, or none if it finished before emitting n values.

This function requires a Productive instance proving that the iterator will always emit a value after a finite number of skips. If the iterator is not productive or such an instance is not available, consider using it.allowNontermination.atIdxSlow? instead of it.atIdxSlow?. However, it is not possible to formally verify the behavior of the partial variant.

21.3.3. Consuming Monadic Iterators

🔗def
Std.Iterators.IterM.drain.{w, w'} {α : Type w} {m : Type w → Type w'}
  [Monad m] {β : Type w} [Iterator α m β] [Finite α m] (it : IterM m β)
  [IteratorLoop α m m] : m PUnit
Std.Iterators.IterM.drain.{w, w'}
  {α : Type w} {m : Type w → Type w'}
  [Monad m] {β : Type w} [Iterator α m β]
  [Finite α m] (it : IterM m β)
  [IteratorLoop α m m] : m PUnit

Iterates over the whole iterator, applying the monadic effects of each step, discarding all emitted values.

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.drain instead of it.drain. However, it is not possible to formally verify the behavior of the partial variant.

🔗def
Std.Iterators.IterM.fold.{w, w'} {m : Type w → Type w'} {α β γ : Type w}
  [Monad m] [Iterator α m β] [Finite α m] [IteratorLoop α m m]
  (f : γ → β → γ) (init : γ) (it : IterM m β) : m γ
Std.Iterators.IterM.fold.{w, w'}
  {m : Type w → Type w'} {α β γ : Type w}
  [Monad m] [Iterator α m β] [Finite α m]
  [IteratorLoop α m m] (f : γ → β → γ)
  (init : γ) (it : IterM m β) : m γ

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.

🔗def
Std.Iterators.IterM.foldM.{w, w', w''} {m : Type w → Type w'}
  {n : Type w → Type w''} [Monad n] {α β γ : Type w} [Iterator α m β]
  [Finite α m] [IteratorLoop α m n] [MonadLiftT m n] (f : γ → β → n γ)
  (init : γ) (it : IterM m β) : n γ
Std.Iterators.IterM.foldM.{w, w', w''}
  {m : Type w → Type w'}
  {n : Type w → Type w''} [Monad n]
  {α β γ : Type w} [Iterator α m β]
  [Finite α m] [IteratorLoop α m n]
  [MonadLiftT m n] (f : γ → β → n γ)
  (init : γ) (it : IterM m β) : n γ

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.

The monadic effects of f are interleaved with potential effects caused by the iterator's step function. Therefore, it may not be 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.

🔗def
Std.Iterators.IterM.count.{w, w'} {α : Type w} {m : Type w → Type w'}
  {β : Type w} [Iterator α m β] [Finite α m] [IteratorLoop α m m]
  [Monad m] (it : IterM m β) : m (ULift Nat)
Std.Iterators.IterM.count.{w, w'}
  {α : Type w} {m : Type w → Type w'}
  {β : Type w} [Iterator α m β]
  [Finite α m] [IteratorLoop α m m]
  [Monad m] (it : IterM m β) :
  m (ULift Nat)

Steps through the whole iterator, counting the number of outputs emitted.

Performance:

This function's runtime is linear in the number of steps taken by the iterator.

🔗def
Std.Iterators.IterM.any.{w, w'} {α β : Type w} {m : Type w → Type w'}
  [Monad m] [Iterator α m β] [IteratorLoop α m m] [Finite α m]
  (p : β → Bool) (it : IterM m β) : m (ULift Bool)
Std.Iterators.IterM.any.{w, w'}
  {α β : Type w} {m : Type w → Type w'}
  [Monad m] [Iterator α m β]
  [IteratorLoop α m m] [Finite α m]
  (p : β → Bool) (it : IterM m β) :
  m (ULift Bool)

Returns ULift.up true if the pure predicate p returns true for any element emitted by the iterator it.

O(|xs|). Short-circuits upon encountering the first match. The elements in it are examined in order of iteration.

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.any instead of it.any. However, it is not possible to formally verify the behavior of the partial variant.

🔗def
Std.Iterators.IterM.anyM.{w, w'} {α β : Type w} {m : Type w → Type w'}
  [Monad m] [Iterator α m β] [IteratorLoop α m m] [Finite α m]
  (p : β → m (ULift Bool)) (it : IterM m β) : m (ULift Bool)
Std.Iterators.IterM.anyM.{w, w'}
  {α β : Type w} {m : Type w → Type w'}
  [Monad m] [Iterator α m β]
  [IteratorLoop α m m] [Finite α m]
  (p : β → m (ULift Bool))
  (it : IterM m β) : m (ULift Bool)

Returns ULift.up true if the monadic predicate p returns ULift.up true for any element emitted by the iterator it.

O(|xs|). Short-circuits upon encountering the first match. The elements in it are examined in order of iteration.

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.anyM instead of it.anyM. However, it is not possible to formally verify the behavior of the partial variant.

🔗def
Std.Iterators.IterM.all.{w, w'} {α β : Type w} {m : Type w → Type w'}
  [Monad m] [Iterator α m β] [IteratorLoop α m m] [Finite α m]
  (p : β → Bool) (it : IterM m β) : m (ULift Bool)
Std.Iterators.IterM.all.{w, w'}
  {α β : Type w} {m : Type w → Type w'}
  [Monad m] [Iterator α m β]
  [IteratorLoop α m m] [Finite α m]
  (p : β → Bool) (it : IterM m β) :
  m (ULift Bool)

Returns ULift.up true if the pure predicate p returns true for all elements emitted by the iterator it.

O(|xs|). Short-circuits upon encountering the first mismatch. The elements in it are examined in order of iteration.

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.all instead of it.all. However, it is not possible to formally verify the behavior of the partial variant.

🔗def
Std.Iterators.IterM.allM.{w, w'} {α β : Type w} {m : Type w → Type w'}
  [Monad m] [Iterator α m β] [IteratorLoop α m m] [Finite α m]
  (p : β → m (ULift Bool)) (it : IterM m β) : m (ULift Bool)
Std.Iterators.IterM.allM.{w, w'}
  {α β : Type w} {m : Type w → Type w'}
  [Monad m] [Iterator α m β]
  [IteratorLoop α m m] [Finite α m]
  (p : β → m (ULift Bool))
  (it : IterM m β) : m (ULift Bool)

Returns ULift.up true if the monadic predicate p returns ULift.up true for all elements emitted by the iterator it.

O(|xs|). Short-circuits upon encountering the first mismatch. The elements in it are examined in order of iteration.

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.allM instead of it.allM. However, it is not possible to formally verify the behavior of the partial variant.

🔗def
Std.Iterators.IterM.find?.{w, w'} {α β : Type w} {m : Type w → Type w'}
  [Monad m] [Iterator α m β] [IteratorLoop α m m] [Finite α m]
  (it : IterM m β) (f : β → Bool) : m (Option β)
Std.Iterators.IterM.find?.{w, w'}
  {α β : Type w} {m : Type w → Type w'}
  [Monad m] [Iterator α m β]
  [IteratorLoop α m m] [Finite α m]
  (it : IterM m β) (f : β → Bool) :
  m (Option β)
🔗def
Std.Iterators.IterM.findM?.{w, w'} {α β : Type w} {m : Type w → Type w'}
  [Monad m] [Iterator α m β] [IteratorLoop α m m] [Finite α m]
  (it : IterM m β) (f : β → m (ULift Bool)) : m (Option β)
Std.Iterators.IterM.findM?.{w, w'}
  {α β : Type w} {m : Type w → Type w'}
  [Monad m] [Iterator α m β]
  [IteratorLoop α m m] [Finite α m]
  (it : IterM m β)
  (f : β → m (ULift Bool)) : m (Option β)
🔗def
Std.Iterators.IterM.findSome?.{w, w'} {α β γ : Type w}
  {m : Type w → Type w'} [Monad m] [Iterator α m β] [IteratorLoop α m m]
  [Finite α m] (it : IterM m β) (f : β → Option γ) : m (Option γ)
Std.Iterators.IterM.findSome?.{w, w'}
  {α β γ : Type w} {m : Type w → Type w'}
  [Monad m] [Iterator α m β]
  [IteratorLoop α m m] [Finite α m]
  (it : IterM m β) (f : β → Option γ) :
  m (Option γ)
🔗def
Std.Iterators.IterM.findSomeM?.{w, w'} {α β γ : Type w}
  {m : Type w → Type w'} [Monad m] [Iterator α m β] [IteratorLoop α m m]
  [Finite α m] (it : IterM m β) (f : β → m (Option γ)) : m (Option γ)
Std.Iterators.IterM.findSomeM?.{w, w'}
  {α β γ : Type w} {m : Type w → Type w'}
  [Monad m] [Iterator α m β]
  [IteratorLoop α m m] [Finite α m]
  (it : IterM m β)
  (f : β → m (Option γ)) : m (Option γ)
🔗def
Std.Iterators.IterM.atIdx?.{u_1, u_2} {α : Type u_1}
  {m : Type u_1 → Type u_2} {β : Type u_1} [Iterator α m β]
  [IteratorAccess α m] [Monad m] (it : IterM m β) (n : Nat) :
  m (Option β)
Std.Iterators.IterM.atIdx?.{u_1, u_2}
  {α : Type u_1} {m : Type u_1 → Type u_2}
  {β : Type u_1} [Iterator α m β]
  [IteratorAccess α m] [Monad m]
  (it : IterM m β) (n : Nat) :
  m (Option β)

Returns the n-th value emitted by it, or none if it terminates earlier.

For monadic iterators, the monadic effects of this operation may differ from manually iterating to the n-th value because atIdx? can take shortcuts. By the signature, the return value is guaranteed to plausible in the sense of IterM.IsPlausibleNthOutputStep.

This function is only available for iterators that explicitly support it by implementing the IteratorAccess typeclass.

21.3.4. Collectors

Collectors consume an iterator, returning all of its data in a list or array. To be collected, an iterator must be finite and have an IteratorCollect or IteratorCollectPartial instance.

🔗def
Std.Iterators.Iter.toArray.{w} {α β : Type w} [Iterator α Id β]
  [Finite α Id] [IteratorCollect α Id Id] (it : Iter β) : Array β
Std.Iterators.Iter.toArray.{w}
  {α β : Type w} [Iterator α Id β]
  [Finite α Id] [IteratorCollect α Id Id]
  (it : Iter β) : Array β

Traverses the given iterator and stores the emitted values in an array.

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.toArray instead of it.toArray. However, it is not possible to formally verify the behavior of the partial variant.

🔗def
Std.Iterators.IterM.toArray.{w, w'} {α β : Type w}
  {m : Type w → Type w'} [Monad m] [Iterator α m β] [Finite α m]
  [IteratorCollect α m m] (it : IterM m β) : m (Array β)
Std.Iterators.IterM.toArray.{w, w'}
  {α β : Type w} {m : Type w → Type w'}
  [Monad m] [Iterator α m β] [Finite α m]
  [IteratorCollect α m m]
  (it : IterM m β) : m (Array β)

Traverses the given iterator and stores the emitted values in an array.

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.toArray instead of it.toArray. However, it is not possible to formally verify the behavior of the partial variant.

🔗def
Std.Iterators.Iter.toList.{w} {α β : Type w} [Iterator α Id β]
  [Finite α Id] [IteratorCollect α Id Id] (it : Iter β) : List β
Std.Iterators.Iter.toList.{w}
  {α β : Type w} [Iterator α Id β]
  [Finite α Id] [IteratorCollect α Id Id]
  (it : Iter β) : List β

Traverses the given iterator and stores the emitted values in a list. Because lists are prepend-only, toListRev is usually more efficient that toList.

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.toList instead of it.toList. However, it is not possible to formally verify the behavior of the partial variant.

🔗def
Std.Iterators.IterM.toList.{w, w'} {α : Type w} {m : Type w → Type w'}
  [Monad m] {β : Type w} [Iterator α m β] [Finite α m]
  [IteratorCollect α m m] (it : IterM m β) : m (List β)
Std.Iterators.IterM.toList.{w, w'}
  {α : Type w} {m : Type w → Type w'}
  [Monad m] {β : Type w} [Iterator α m β]
  [Finite α m] [IteratorCollect α m m]
  (it : IterM m β) : m (List β)

Traverses the given iterator and stores the emitted values in a list. Because lists are prepend-only, toListRev is usually more efficient that toList.

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.toList instead of it.toList. However, it is not possible to formally verify the behavior of the partial variant.

🔗def
Std.Iterators.Iter.toListRev.{w} {α β : Type w} [Iterator α Id β]
  [Finite α Id] (it : Iter β) : List β
Std.Iterators.Iter.toListRev.{w}
  {α β : Type w} [Iterator α Id β]
  [Finite α Id] (it : Iter β) : List β

Traverses the given iterator and stores the emitted values in reverse order in a list. Because lists are prepend-only, this toListRev is usually more efficient that toList.

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.toListRev instead of it.toListRev. However, it is not possible to formally verify the behavior of the partial variant.

🔗def
Std.Iterators.IterM.toListRev.{w, w'} {α : Type w}
  {m : Type w → Type w'} [Monad m] {β : Type w} [Iterator α m β]
  [Finite α m] (it : IterM m β) : m (List β)
Std.Iterators.IterM.toListRev.{w, w'}
  {α : Type w} {m : Type w → Type w'}
  [Monad m] {β : Type w} [Iterator α m β]
  [Finite α m] (it : IterM m β) :
  m (List β)

Traverses the given iterator and stores the emitted values in reverse order in a list. Because lists are prepend-only, this toListRev is usually more efficient that toList.

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.toListRev instead of it.toListRev. However, it is not possible to formally verify the behavior of the partial variant.

🔗type class
Std.Iterators.IteratorCollect.{w, w', w''} (α : Type w)
  (m : Type w → Type w') (n : Type w → Type w'') {β : Type w}
  [Iterator α m β] : Type (max (max (w + 1) w') w'')
Std.Iterators.IteratorCollect.{w, w', w''}
  (α : Type w) (m : Type w → Type w')
  (n : Type w → Type w'') {β : Type w}
  [Iterator α m β] :
  Type (max (max (w + 1) w') w'')

IteratorCollect α m provides efficient implementations of collectors for α-based iterators. Right now, it is limited to a potentially optimized toArray implementation.

This class is experimental and users of the iterator API should not explicitly depend on it. They can, however, assume that consumers that require an instance will work for all iterators provided by the standard library.

Note: For this to be compositional enough to be useful, toArrayMapped would need to accept a termination proof for the specific mapping function used instead of the blanket Finite α m instance. Otherwise, most combinators like map cannot implement their own instance relying on the instance of their base iterators. However, fixing this is currently low priority.

Instance Constructor

Std.Iterators.IteratorCollect.mk.{w, w', w''}

Methods

toArrayMapped : [Finite α m] → (⦃δ : Type w⦄ → m δ → n δ) → {γ : Type w} → (β → n γ) → IterM m β → n (Array γ)

Maps the emitted values of an iterator using the given function and collects the results in an Array. This is an internal implementation detail. Consider using it.map f |>.toArray instead.

🔗def
Std.Iterators.IteratorCollect.defaultImplementation.{w, w', w''}
  {α β : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
  [Monad n] [Iterator α m β] : IteratorCollect α m n
Std.Iterators.IteratorCollect.defaultImplementation.{w,
    w', w''}
  {α β : Type w} {m : Type w → Type w'}
  {n : Type w → Type w''} [Monad n]
  [Iterator α m β] : IteratorCollect α m n

This is the default implementation of the IteratorLoop class. It simply iterates through the iterator using IterM.step, incrementally building up the desired data structure. For certain iterators, more efficient implementations are possible and should be used instead.

🔗type class
Std.Iterators.LawfulIteratorCollect.{w, w', w''} (α : Type w)
  (m : Type w → Type w') (n : Type w → Type w'') {β : Type w} [Monad m]
  [Monad n] [Iterator α m β] [i : IteratorCollect α m n] : Prop
Std.Iterators.LawfulIteratorCollect.{w,
    w', w''}
  (α : Type w) (m : Type w → Type w')
  (n : Type w → Type w'') {β : Type w}
  [Monad m] [Monad n] [Iterator α m β]
  [i : IteratorCollect α m n] : Prop

Asserts that a given IteratorCollect instance is equal to IteratorCollect.defaultImplementation. (Even though equal, the given instance might be vastly more efficient.)

Instance Constructor

Std.Iterators.LawfulIteratorCollect.mk.{w, w', w''}

Methods

lawful_toArrayMapped : ∀ {γ : Type w} (lift : ⦃α : Type w⦄ → m α → n α) [Std.Internal.LawfulMonadLiftFunction lift] [inst : Finite α m],
  IteratorCollect.toArrayMapped lift = IteratorCollect.toArrayMapped lift
🔗type class
Std.Iterators.IteratorCollectPartial.{w, w', w''} (α : Type w)
  (m : Type w → Type w') (n : Type w → Type w'') {β : Type w}
  [Iterator α m β] : Type (max (max (w + 1) w') w'')
Std.Iterators.IteratorCollectPartial.{w,
    w', w''}
  (α : Type w) (m : Type w → Type w')
  (n : Type w → Type w'') {β : Type w}
  [Iterator α m β] :
  Type (max (max (w + 1) w') w'')

IteratorCollectPartial α m provides efficient implementations of collectors for α-based iterators. Right now, it is limited to a potentially optimized partial toArray implementation.

This class is experimental and users of the iterator API should not explicitly depend on it. They can, however, assume that consumers that require an instance will work for all iterators provided by the standard library.

Instance Constructor

Std.Iterators.IteratorCollectPartial.mk.{w, w', w''}

Methods

toArrayMappedPartial : (⦃δ : Type w⦄ → m δ → n δ) → {γ : Type w} → (β → n γ) → IterM m β → n (Array γ)

Maps the emitted values of an iterator using the given function and collects the results in an Array. This is an internal implementation detail. Consider using it.map f |>.allowNontermination.toArray instead.

🔗def
Std.Iterators.IteratorCollectPartial.defaultImplementation.{w, w', w''}
  {α β : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
  [Monad n] [Iterator α m β] : IteratorCollectPartial α m n
Std.Iterators.IteratorCollectPartial.defaultImplementation.{w,
    w', w''}
  {α β : Type w} {m : Type w → Type w'}
  {n : Type w → Type w''} [Monad n]
  [Iterator α m β] :
  IteratorCollectPartial α m n

This is the default implementation of the IteratorLoopPartial class. It simply iterates through the iterator using IterM.step, incrementally building up the desired data structure. For certain iterators, more efficient implementations are possible and should be used instead.