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 type class.

@[inline]

def Std.Iterators.Iter.instForIn' {α β : Type w} {n : Type x → Type x'} [Monad n] [Iterator α 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.instForInIterOfMonadOfIteratorLoopId (α β : Type w) (n : Type x → Type x') [Monad n] [Iterator α Id β] [IteratorLoop α Id n] : ForIn n (Iter β) β

Equations

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

@[inline]

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

An implementation of for h : ... in ... do ... notation for partial iterators.

Equations

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

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

Equations

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

@[inline]

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

A ForIn' instance for iterators that is guaranteed to terminate after finitely many steps. It is not marked as an instance because the membership predicate is difficult to work with.

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

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 β] [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.

Equations

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

@[inline, deprecated Std.Iterators.Iter.foldM (since := "2025-12-04")]

def Std.Iterators.Iter.Partial.foldM {m : Type x → Type x'} [Monad m] {α β : Type w} {γ : Type x} [Iterator α Id β] [IteratorLoop α 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 function is deprecated. Instead of it.allowNontermination.foldM, use it.foldM.

Equations

• Std.Iterators.Iter.Partial.foldM f init it = Std.Iterators.Iter.foldM f init it.it

@[inline]

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

Equations

• Std.Iterators.Iter.Total.foldM f init it = Std.Iterators.Iter.foldM f init it.it

@[inline]

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

Equations

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

@[inline, deprecated Std.Iterators.Iter.fold (since := "2025-12-04")]

def Std.Iterators.Iter.Partial.fold {α β : Type w} {γ : Type x} [Iterator α Id β] [IteratorLoop α 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 function is deprecated. Instead of it.allowNontermination.fold, use it.fold.

Equations

• Std.Iterators.Iter.Partial.fold f init it = Std.Iterators.Iter.fold f init it.it

@[inline]

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

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 variant terminates after finitely many steps and requires a proof that the iterator is finite. If such a proof is not available, consider using Iter.fold.

Equations

• Std.Iterators.Iter.Total.fold f init it = Std.Iterators.Iter.fold f init it.it

@[always_inline]

def Std.Iterators.Iter.anyM {α β : Type w} {m : Type → Type w'} [Monad m] [Iterator α Id β] [IteratorLoop α Id m] (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.Total.anyM {α β : Type w} {m : Type → Type w'} [Monad m] [Iterator α Id β] [IteratorLoop α Id m] [Finite α Id] (p : β → m Bool) (it : Total β) : 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.

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 Iter.anyM.

Equations

• Std.Iterators.Iter.Total.anyM p it = Std.Iterators.Iter.anyM p it.it

@[inline]

def Std.Iterators.Iter.any {α β : Type w} [Iterator α Id β] [IteratorLoop α Id 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

@[inline]

def Std.Iterators.Iter.Total.any {α β : Type w} [Iterator α Id β] [IteratorLoop α Id Id] [Finite α Id] (p : β → Bool) (it : Total β) : 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.

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 Iter.any.

Equations

• Std.Iterators.Iter.Total.any p it = Std.Iterators.Iter.any p it.it

@[inline]

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

Returns true if the monadic predicate p returns true for all 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.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.Total.allM {α β : Type w} {m : Type → Type w'} [Monad m] [Iterator α Id β] [IteratorLoop α Id m] [Finite α Id] (p : β → m Bool) (it : Total β) : m Bool

Returns true if the monadic predicate p returns true for all 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 variant terminates after finitely mall steps and requires a proof that the iterator is finite. If such a proof is not available, consider using Iter.allM.

Equations

• Std.Iterators.Iter.Total.allM p it = Std.Iterators.Iter.allM p it.it

@[inline]

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

Returns true if the pure predicate p returns true for all 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.all p it = (Std.Iterators.Iter.allM (fun (x : β) => pure (p x)) it).run

@[inline]

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

Returns true if the pure predicate p returns true for all 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 variant terminates after finitely mall steps and requires a proof that the iterator is finite. If such a proof is not available, consider using Iter.all.

Equations

• Std.Iterators.Iter.Total.all p it = Std.Iterators.Iter.all p it.it

@[inline]

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

Returns the first non-none result of applying the monadic function f to each output of the iterator, in order. Returns none if f returns none for all outputs.

O(|it|). Short-circuits when f returns some _. The outputs of it are examined in order of iteration.

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

Example:

#eval [7, 6, 5, 8, 1, 2, 6].iter.findSomeM? fun i => do
  if i < 5 then
    return some (i * 10)
  if i ≤ 6 then
    IO.println s!"Almost! {i}"
  return none

Almost! 6
Almost! 5

some 10

Equations

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

@[inline, deprecated Std.Iterators.Iter.findSomeM? (since := "2025-12-04")]

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

Returns the first non-none result of applying the monadic function f to each output of the iterator, in order. Returns none if f returns none for all outputs.

O(|it|). Short-circuits when f returns some _. The outputs of it are examined in order of iteration.

This function is deprecated. Instead of it.allowNontermination.findSomeM?, use it.findSomeM?.

Example:

#eval [7, 6, 5, 8, 1, 2, 6].iter.findSomeM? fun i => do
  if i < 5 then
    return some (i * 10)
  if i ≤ 6 then
    IO.println s!"Almost! {i}"
  return none

Almost! 6
Almost! 5

some 10

Equations

• it.findSomeM? f = it.it.findSomeM? f

@[inline]

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

Returns the first non-none result of applying the monadic function f to each output of the iterator, in order. Returns none if f returns none for all outputs.

O(|it|). Short-circuits when f returns some _. The outputs of it are examined in order of iteration.

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 Iter.findSomeM?.

Example:

#eval [7, 6, 5, 8, 1, 2, 6].iter.findSomeM? fun i => do
  if i < 5 then
    return some (i * 10)
  if i ≤ 6 then
    IO.println s!"Almost! {i}"
  return none

Almost! 6
Almost! 5

some 10

Equations

• it.findSomeM? f = it.it.findSomeM? f

@[inline]

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

Returns the first non-none result of applying f to each output of the iterator, in order. Returns none if f returns none for all outputs.

O(|it|). Short-circuits when f returns some _.The outputs of it are examined in order of iteration.

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

Examples:

• [7, 6, 5, 8, 1, 2, 6].iter.findSome? (fun x => if x < 5 then some (10 * x) else none) = some 10
• [7, 6, 5, 8, 1, 2, 6].iter.findSome? (fun x => if x < 1 then some (10 * x) else none) = none

Equations

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

@[inline, deprecated Std.Iterators.Iter.findSome? (since := "2025-12-04")]

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

Returns the first non-none result of applying f to each output of the iterator, in order. Returns none if f returns none for all outputs.

O(|it|). Short-circuits when f returns some _.The outputs of it are examined in order of iteration.

This function is deprecated. Instead of it.allowNontermination.findSome?, use it.findSome?.

Examples:

• [7, 6, 5, 8, 1, 2, 6].iter.allowNontermination.findSome? (fun x => if x < 5 then some (10 * x) else none) = some 10
• [7, 6, 5, 8, 1, 2, 6].iter.allowNontermination.findSome? (fun x => if x < 1 then some (10 * x) else none) = none

Equations

• it.findSome? f = it.it.findSome? f

@[inline]

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

Returns the first non-none result of applying f to each output of the iterator, in order. Returns none if f returns none for all outputs.

O(|it|). Short-circuits when f returns some _.The outputs of it are examined in order of iteration.

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 Iter.findSome?.

Examples:

• [7, 6, 5, 8, 1, 2, 6].iter.ensureTermination.findSome? (fun x => if x < 5 then some (10 * x) else none) = some 10
• [7, 6, 5, 8, 1, 2, 6].iter.ensureTermination.findSome? (fun x => if x < 1 then some (10 * x) else none) = none

Equations

• it.findSome? f = it.it.findSome? f

@[inline]

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

Returns the first output of the iterator for which the monadic predicate p returns true, or none if no such element is found.

O(|it|). Short-circuits when f returns true. The outputs of it are examined in order of iteration.

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

Example:

#eval [7, 6, 5, 8, 1, 2, 6].iter.findM? fun i => do
  if i < 5 then
    return true
  if i ≤ 6 then
    IO.println s!"Almost! {i}"
  return false

Almost! 6
Almost! 5

some 1

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, deprecated Std.Iterators.Iter.findM? (since := "2025-12-04")]

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

Returns the first output of the iterator for which the monadic predicate p returns true, or none if no such element is found.

O(|it|). Short-circuits when f returns true. The outputs of it are examined in order of iteration.

This function is deprecated. Instead of it.ensureTermination.findM?, use it.findM?.

Example:

#eval [7, 6, 5, 8, 1, 2, 6].iter.findM? fun i => do
  if i < 5 then
    return true
  if i ≤ 6 then
    IO.println s!"Almost! {i}"
  return false

Almost! 6
Almost! 5

some 1

Equations

• it.findM? f = it.it.findM? f

@[inline]

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

Returns the first output of the iterator for which the monadic predicate p returns true, or none if no such element is found.

O(|it|). Short-circuits when f returns true. The outputs of it are examined in order of iteration.

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

Example:

#eval [7, 6, 5, 8, 1, 2, 6].iter.findM? fun i => do
  if i < 5 then
    return true
  if i ≤ 6 then
    IO.println s!"Almost! {i}"
  return false

Almost! 6
Almost! 5

some 1

Equations

• it.findM? f = it.it.findM? f

@[inline]

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

Returns the first output of the iterator for which the predicate p returns true, or none if no such output is found.

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

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

Examples:

• [7, 6, 5, 8, 1, 2, 6].iter.find? (· < 5) = some 1
• [7, 6, 5, 8, 1, 2, 6].iter.find? (· < 1) = none

Equations

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

@[inline, deprecated Std.Iterators.Iter.find? (since := "2025-12-04")]

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

Returns the first output of the iterator for which the predicate p returns true, or none if no such output is found.

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

This function is deprecated. Instead of it.allowNontermination.find?, use it.find?.

Examples:

• [7, 6, 5, 8, 1, 2, 6].iter.allowNontermination.find? (· < 5) = some 1
• [7, 6, 5, 8, 1, 2, 6].iter.allowNontermination.find? (· < 1) = none

Equations

• it.find? f = it.it.find? f

@[inline]

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

Returns the first output of the iterator for which the predicate p returns true, or none if no such output is found.

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

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 Iter.find?.

Examples:

• [7, 6, 5, 8, 1, 2, 6].iter.find? (· < 5) = some 1
• [7, 6, 5, 8, 1, 2, 6].iter.find? (· < 1) = none

Equations

• it.find? f = it.it.find? f

@[inline]

def Std.Iterators.Iter.count {α β : Type w} [Iterator α 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 β] [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, deprecated Std.Iterators.Iter.count (since := "2025-12-04")]

def Std.Iterators.Iter.Partial.count {α β : Type w} [Iterator α Id β] [IteratorLoop α 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.count.run.down

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

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