Collectors

This module provides consumers that collect the values emitted by an iterator in a data structure. Concretely, the following operations are provided:

• IterM.toList, collecting the values in a list
• IterM.toListRev, collecting the values in a list in reverse order but more efficiently
• IterM.toArray, collecting the values in an array

def Std.IterM.toArray.RecursionRel {α β : Type w} {m : Type w → Type w'} [Iterator α m β] {γ : Type w} (x' x : (_ : IterM m β) ×' Array γ) : Prop

If this relation is well-founded, then IterM.toArray, IterM.toList and IterM.toListRev are guaranteed to finish after finitely many steps. If all of the iterator's steps terminate individually, IterM.toArray is guaranteed to terminate.

Equations

• One or more equations did not get rendered due to their size.

@[inline]

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

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

If the iterator is not finite, this function might run forever. The variant it.ensureTermination.toArray always terminates after finitely many steps.

Equations

• it.toArray = Std.IterM.toArray.go it #[]

@[always_inline]

def Std.IterM.toArray.go {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] (it : IterM m β) (acc : Array β) : m (Array β)

Equations

• One or more equations did not get rendered due to their size.

@[inline, deprecated Std.IterM.toArray (since := "2025-10-23")]

def Std.IterM.Partial.toArray {α : Type w} {m : Type w → Type w'} {β : Type w} [Monad m] [Iterator α m β] (it : Partial m β) : m (Array β)

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

This function is deprecated. Instead of it.allowNontermination.toArray, use it.toArray.

Equations

• it.toArray = it.it.toArray

@[inline]

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

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

This variant terminates after finitely many steps and requires a proof that the iterator is finite. If such a proof is not available, consider using IterM.toArray.

Equations

• it.toArray = it.it.toArray

@[inline]

def Std.IterM.toListRev {α : Type w} {m : Type w → Type w'} [Monad m] {β : Type w} [Iterator α 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.

If the iterator is not finite, this function might run forever. The variant it.ensureTermination.toListRev always terminates after finitely many steps.

Equations

• it.toListRev = Std.IterM.toListRev.go it []

@[inline]

def Std.IterM.toListRev.go {α : Type w} {m : Type w → Type w'} [Monad m] {β : Type w} [Iterator α m β] (it : IterM m β) (acc : List β) : m (List β)

Equations

• One or more equations did not get rendered due to their size.

@[inline, deprecated Std.IterM.toListRev (since := "2025-10-23")]

def Std.IterM.Partial.toListRev {α : Type w} {m : Type w → Type w'} [Monad m] {β : Type w} [Iterator α m β] (it : Partial 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 is deprecated. Instead of it.allowNontermination.toListRev, use it.toListRev.

Equations

• it.toListRev = it.it.toListRev

@[inline]

def Std.IterM.Total.toListRev {α : Type w} {m : Type w → Type w'} {β : Type w} [Monad m] [Iterator α m β] [Iterators.Finite α m] (it : Total 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 variant terminates after finitely many steps and requires a proof that the iterator is finite. If such a proof is not available, consider using IterM.toListRev.

Equations

• it.toListRev = it.it.toListRev

@[inline]

def Std.IterM.toList {α : Type w} {m : Type w → Type w'} [Monad m] {β : Type w} [Iterator α 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.

If the iterator is not finite, this function might run forever. The variant it.ensureTermination.toList always terminates after finitely many steps.

Equations

• it.toList = Array.toList <$> it.toArray

@[inline, deprecated Std.IterM.toList (since := "2025-10-23")]

def Std.IterM.Partial.toList {α : Type w} {m : Type w → Type w'} [Monad m] {β : Type w} [Iterator α m β] (it : Partial 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 is deprecated. Instead of it.allowNontermination.toList, use it.toList.

Equations

• it.toList = Array.toList <$> it.it.toArray

@[inline]

def Std.IterM.Total.toList {α : Type w} {m : Type w → Type w'} {β : Type w} [Monad m] [Iterator α m β] [Iterators.Finite α m] (it : Total 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 variant terminates after finitely many steps and requires a proof that the iterator is finite. If such a proof is not available, consider using IterM.toList.

Equations

• it.toList = it.it.toList