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:

• ForIn instances
• Iter.fold, the analogue of List.foldl
• Iter.foldM, the analogue of List.foldlM

These operations are implemented using the IteratorLoop and IteratorLoopPartial typeclasses.

@[inline]

def Std.Iterators.Iter.instForIn' {α β : Type w} {n : Type x → Type x'} [Monad n] [Iterator α Id β] [Finite α Id] [IteratorLoop α Id n] : ForIn' n (Iter β) β { mem := fun (it : Iter β) (out : β) => it.IsPlausibleIndirectOutput out }

A ForIn' instance for iterators. Its generic membership relation is not easy to use, so this is not marked as instance. This way, more convenient instances can be built on top of it or future library improvements will make it more comfortable.

Equations

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

instance Std.Iterators.instForInIterOfMonadOfFiniteOfIteratorLoopId (α β : Type w) (n : Type x → Type x') [Monad n] [Iterator α Id β] [Finite α Id] [IteratorLoop α Id n] : ForIn n (Iter β) β

Equations

• Std.Iterators.instForInIterOfMonadOfFiniteOfIteratorLoopId α β n = instForInOfForIn'

@[inline]

def Std.Iterators.Iter.Partial.instForIn' {α β : Type w} {n : Type x → Type x'} [Monad n] [Iterator α Id β] [IteratorLoopPartial α Id n] : ForIn' n (Partial β) β { mem := fun (it : Partial β) (out : β) => it.it.IsPlausibleIndirectOutput out }

Equations

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

instance Std.Iterators.instForInPartialOfMonadOfIteratorLoopPartialId (α β : Type w) (n : Type x → Type x') [Monad n] [Iterator α Id β] [IteratorLoopPartial α Id n] : ForIn n (Iter.Partial β) β

Equations

• Std.Iterators.instForInPartialOfMonadOfIteratorLoopPartialId α β n = instForInOfForIn'

instance Std.Iterators.instForMIterOfFiniteOfIteratorLoopId {m : Type x → Type x'} {α β : Type w} [Iterator α Id β] [Finite α Id] [IteratorLoop α Id m] : ForM m (Iter β) β

Equations

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

instance Std.Iterators.instForMPartialOfFiniteOfIteratorLoopPartialId {m : Type x → Type x'} {α β : Type w} [Iterator α Id β] [Finite α Id] [IteratorLoopPartial α Id m] : ForM m (Iter.Partial β) β

Equations

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

@[inline]

def Std.Iterators.Iter.foldM {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.

Equations

• Std.Iterators.Iter.foldM f init it = forIn it init fun (x : β) (acc : γ) => ForInStep.yield <$> f acc x

@[inline]

def Std.Iterators.Iter.Partial.foldM {m : Type x → Type x'} [Monad m] {α β : Type w} {γ : Type x} [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

• Std.Iterators.Iter.Partial.foldM f init it = forIn it init fun (x : β) (acc : γ) => ForInStep.yield <$> f acc x

@[inline]

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

Equations

• Std.Iterators.Iter.fold f init it = forIn it init fun (x : β) (acc : γ) => ForInStep.yield (f acc x)

@[inline]

def Std.Iterators.Iter.Partial.fold {α β : Type w} {γ : Type x} [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

• Std.Iterators.Iter.Partial.fold f init it = forIn it init fun (x : β) (acc : γ) => ForInStep.yield (f acc x)

@[specialize #[]]

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

Equations

• Std.Iterators.Iter.anyM p it = forIn it false fun (x : β) (x_1 : Bool) => do let __do_lift ← p x if __do_lift = true then pure (ForInStep.done true) else pure (ForInStep.yield false)

@[inline]

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

Equations

• Std.Iterators.Iter.any p it = (Std.Iterators.Iter.anyM (fun (x : β) => pure (p x)) it).run

@[specialize #[]]

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

Equations

• Std.Iterators.Iter.allM p it = forIn it true fun (x : β) (x_1 : Bool) => do let __do_lift ← p x if __do_lift = true then pure (ForInStep.yield true) else pure (ForInStep.done false)

@[inline]

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

Equations

• Std.Iterators.Iter.all p it = (Std.Iterators.Iter.allM (fun (x : β) => pure (p x)) it).run

@[inline]

def Std.Iterators.Iter.findSomeM? {α β : 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 γ)

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

• it.findSome? f = (it.findSomeM? fun (x : β) => pure (f x)).run

@[inline]

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

Equations

• it.findSome? f = (it.findSomeM? fun (x : β) => pure (f x)).run

@[inline]

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

Equations

• it.findM? f = it.findSomeM? fun (x : β) => do let __do_lift ← f x pure (if __do_lift.down = true then some x else none)

@[inline]

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

Equations

• it.findM? f = it.findSomeM? fun (x : β) => do let __do_lift ← f x pure (if __do_lift.down = true then some x else none)

@[inline]

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

Equations

• it.find? f = (it.findM? fun (x : β) => pure { down := f x }).run

@[inline]

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

Equations

• it.find? f = (it.findM? fun (x : β) => pure { down := f x }).run

@[inline]

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

Equations

• it.count = it.toIterM.count.run.down

@[inline, deprecated Std.Iterators.Iter.count (since := "2025-10-29")]

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

Equations

• it.size = it.count

@[inline]

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

Equations

• it.count = it.it.toIterM.allowNontermination.count.run.down

@[inline, deprecated Std.Iterators.Iter.Partial.count (since := "2025-10-29")]

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

Equations

• it.size = it.count