Collectors

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

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

Some operations are implemented using the IteratorCollect and IteratorCollectPartial typeclasses.

@[inline]

def Std.Iterators.Iter.toArray {α β : 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.

Equations

• it.toArray = it.toIterM.toArray.run

@[inline]

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

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

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.toArray instead.

Equations

• it.toArray = it.it.toIterM.allowNontermination.toArray.run

@[inline]

def Std.Iterators.Iter.toListRev {α β : 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.

Equations

• it.toListRev = it.toIterM.toListRev.run

@[inline]

def Std.Iterators.Iter.Partial.toListRev {α β : Type w} [Iterator α Id β] (it : Partial β) : 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 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.toListRev instead.

Equations

• it.toListRev = it.it.toIterM.allowNontermination.toListRev.run

@[inline]

def Std.Iterators.Iter.toList {α β : 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.

Equations

• it.toList = it.toIterM.toList.run

@[inline]

def Std.Iterators.Iter.Partial.toList {α β : Type w} [Iterator α Id β] [IteratorCollectPartial α Id Id] (it : Partial β) : 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 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.toList instead.

Equations

• it.toList = it.it.toIterM.allowNontermination.toList.run