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.

@[implicit_reducible, inline]

def Std.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.

@[implicit_reducible]

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

@[implicit_reducible, inline]

def Std.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.

@[implicit_reducible]

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

@[implicit_reducible, inline]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[inline]

def Std.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.

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

def Std.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.

@[inline]

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

@[inline]

def Std.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.

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

def Std.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.

@[inline]

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

@[always_inline]

def Std.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.

@[inline]

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

@[inline]

def Std.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.

@[inline]

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

@[inline]

def Std.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.

@[inline]

def Std.Iter.Total.allM {α β : Type w} {m : Type → Type w'} [Monad m] [Iterator α Id β] [IteratorLoop α Id m] [Iterators.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.

@[inline]

def Std.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.

@[inline]

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

@[inline]

def Std.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

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

def Std.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

@[inline]

def Std.Iter.Total.findSomeM? {α β : Type w} {γ : Type x} {m : Type x → Type w'} [Monad m] [Iterator α Id β] [IteratorLoop α Id m] [Iterators.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

@[inline]

def Std.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

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

def Std.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

@[inline]

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

@[inline]

def Std.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

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

def Std.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

@[inline]

def Std.Iter.Total.findM? {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α Id β] [IteratorLoop α Id m] [Iterators.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

@[inline]

def Std.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

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

def Std.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

@[inline]

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

@[inline]

def Std.Iter.first? {α β : Type w} [Iterator α Id β] [IteratorLoop α Id Id] (it : Iter β) : Option β

Returns the first output of the iterator, or none if no such output is found.

O(|it|) since the iterator may skip an unknown number of times before returning a result. Short-circuits upon encountering the first result. Only the first element of it is examined.

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

Examples:

• [7, 6].iter.first? = some 7
• [].iter.first? = none

@[inline]

def Std.Iter.Total.first? {α β : Type w} [Iterator α Id β] [IteratorLoop α Id Id] [Iterators.Productive α Id] (it : Total β) : Option β

Returns the first output of the iterator, or none if no such output is found.

O(|it|) since the iterator may skip an unknown number of times before returning a result. Short-circuits upon encountering the first result. 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 productive. If such a proof is not available, consider using Iter.first?.

Examples:

• [7, 6].iter.first? = some 7
• [].iter.first? = none

@[inline]

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

Returns true if the iterator yields no values.

O(|it|) since the iterator may skip an unknown number of times before returning a result. Short-circuits upon encountering the first result. Only the first element of it is examined.

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

Examples:

• [].iter.isEmpty = true
• [1].iter.isEmpty = false

@[inline]

def Std.Iter.Total.isEmpty {α β : Type w} [Iterator α Id β] [IteratorLoop α Id Id] [Iterators.Productive α Id] (it : Total β) : Bool

Returns true if the iterator yields no values.

O(|it|) since the iterator may skip an unknown number of times before returning a result. Short-circuits upon encountering the first result. Only the first element of it is examined.

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

Examples:

• [].iter.isEmpty = true
• [1].iter.isEmpty = false

@[inline]

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

@[inline, deprecated Std.Iter.length (since := "2026-01-28")]

def Std.Iter.count {α β : Type u_1} [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.

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

def Std.Iter.size {α β : Type u_1} [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.

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

def Std.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.

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

def Std.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.