Loop-based 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
• IterM.fold, the analogue of List.foldl
• IterM.foldM, the analogue of List.foldlM
• IterM.drain, which iterates over the whole iterator and discards all emitted values. It can be used to apply the monadic effects of the iterator.

Some producers and combinators provide specialized implementations. These are captured by the IteratorLoop type class. They should be implemented by all types of iterators. A default implementation is provided. The typeclass LawfulIteratorLoop asserts that an IteratorLoop instance equals the default implementation.

def Std.IteratorLoop.rel (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β] {γ : Type x} (plausible_forInStep : β → γ → ForInStep γ → Prop) (p' p : IterM m β × γ) : Prop

Relation that needs to be well-formed in order for a loop over an iterator to terminate. It is assumed that the plausible_forInStep predicate relates the input and output of the stepper function.

def Std.IteratorLoop.WellFounded (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β] {γ : Type x} (plausible_forInStep : β → γ → ForInStep γ → Prop) : Prop

Asserts that IteratorLoop.rel is well-founded.

class Std.IteratorLoop (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β] (n : Type x → Type x') : Type (max (max (max (w + 1) w') (x + 1)) x')

IteratorLoop α m provides efficient implementations of loop-based consumers for α-based iterators. The basis is a ForIn-style loop construct.

Its behavior for well-founded loops is fully characterized by the LawfulIteratorLoop type class.

This class is experimental and users of the iterator API should not explicitly depend on it. They can, however, assume that consumers that require an instance will work for all iterators provided by the standard library.

• forIn (_liftBind : (γ : Type w) → (δ : Type x) → (γ → n δ) → m γ → n δ) (γ : Type x) (plausible_forInStep : β → γ → ForInStep γ → Prop) (it : IterM m β) : γ → ((b : β) → it.IsPlausibleIndirectOutput b → (c : γ) → n (Subtype (plausible_forInStep b c))) → n γ

  Iteration over the iterator it in the manner expected by for loops.

theorem Std.IteratorLoop.ext_iff {α : Type w} {m : Type w → Type w'} {β : Type w} {inst✝ : Iterator α m β} {n : Type x → Type x'} {x y : IteratorLoop α m n} : x = y ↔ forIn = forIn

theorem Std.IteratorLoop.ext {α : Type w} {m : Type w → Type w'} {β : Type w} {inst✝ : Iterator α m β} {n : Type x → Type x'} {x y : IteratorLoop α m n} (forIn : forIn = forIn) : x = y

structure Std.IteratorLoop.WithWF (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β] {γ : Type x} (PlausibleForInStep : β → γ → ForInStep γ → Prop) (hwf : WellFounded α m PlausibleForInStep) : Type (max w x)

Internal implementation detail of the iterator library.

• it : IterM m β

  Internal implementation detail of the iterator library.

• acc : γ

  Internal implementation detail of the iterator library.

instance Std.IteratorLoop.WithWF.instWellFoundedRelation (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β] {γ : Type x} (PlausibleForInStep : β → γ → ForInStep γ → Prop) (hwf : WellFounded α m PlausibleForInStep) : WellFoundedRelation (WithWF α m PlausibleForInStep hwf)

@[inline]

def Std.IterM.DefaultConsumers.forIn' {m : Type w → Type w'} {α β : Type w} [Iterator α m β] {n : Type x → Type x'} [Monad n] (lift : (γ : Type w) → (δ : Type x) → (γ → n δ) → m γ → n δ) (γ : Type x) (PlausibleForInStep : β → γ → ForInStep γ → Prop) (it : IterM m β) (init : γ) (P : β → Prop) (hP : ∀ (b : β), it.IsPlausibleIndirectOutput b → P b) (f : (b : β) → P b → (c : γ) → n (Subtype (PlausibleForInStep b c))) : n γ

This is the loop implementation of the default instance IteratorLoop.defaultImplementation.

@[irreducible, specialize #[]]

def Std.IterM.DefaultConsumers.forIn'.wf {m : Type w → Type w'} {α β : Type w} [Iterator α m β] {n : Type x → Type x'} [Monad n] (lift : (γ : Type w) → (δ : Type x) → (γ → n δ) → m γ → n δ) (γ : Type x) (PlausibleForInStep : β → γ → ForInStep γ → Prop) (wf : IteratorLoop.WellFounded α m PlausibleForInStep) (it : IterM m β) (init : γ) (P : β → Prop) (hP : ∀ (b : β), it.IsPlausibleIndirectOutput b → P b) (f : (b : β) → P b → (c : γ) → n (Subtype (PlausibleForInStep b c))) : n γ

This is the loop implementation of the default instance IteratorLoop.defaultImplementation.

@[inline]

def Std.IteratorLoop.defaultImplementation {β α : Type w} {m : Type w → Type w'} {n : Type x → Type x'} [Monad n] [Iterator α m β] : IteratorLoop α m n

This is the default implementation of the IteratorLoop class. It simply iterates through the iterator using IterM.step. For certain iterators, more efficient implementations are possible and should be used instead.

class Std.LawfulIteratorLoop {β : Type w} (α : Type w) (m : Type w → Type w') (n : Type x → Type x') [Monad m] [Monad n] [Iterator α m β] [i : IteratorLoop α m n] : Prop

Asserts that a given IteratorLoop instance is equal to IteratorLoop.defaultImplementation. (Even though equal, the given instance might be vastly more efficient.)

• lawful (lift : (γ : Type w) → (δ : Type x) → (γ → n δ) → m γ → n δ) [Internal.LawfulMonadLiftBindFunction lift] (γ : Type x) (it : IterM m β) (init : γ) (Pl : β → γ → ForInStep γ → Prop) (wf : IteratorLoop.WellFounded α m Pl) (f : (b : β) → it.IsPlausibleIndirectOutput b → (c : γ) → n (Subtype (Pl b c))) : IteratorLoop.forIn lift γ Pl it init f = IteratorLoop.forIn lift γ Pl it init f

  The implementation of IteratorLoop.forIn in i is equal to the default implementation.

instance Std.instLawfulIteratorLoopDefaultImplementation {β : Type w} (α : Type w) (m : Type w → Type w') (n : Type x → Type x') [Monad m] [Monad n] [Iterator α m β] [Iterators.Finite α m] : LawfulIteratorLoop α m n

theorem Std.IteratorLoop.wellFounded_of_finite {m : Type w → Type w'} {α β : Type w} {γ : Type x} [Iterator α m β] [Iterators.Finite α m] : WellFounded α m fun (x : β) (x_1 : γ) (x_2 : ForInStep γ) => True

@[inline]

def Std.IteratorLoop.finiteForIn' {m : Type w → Type w'} {n : Type x → Type x'} {α β : Type w} [Iterator α m β] [IteratorLoop α m n] [Monad n] (lift : (γ : Type w) → (δ : Type x) → (γ → n δ) → m γ → n δ) : ForIn' n (IterM m β) β { mem := fun (it : IterM m β) (out : β) => it.IsPlausibleIndirectOutput out }

This ForIn'-style loop construct traverses a finite iterator using an IteratorLoop instance.

@[inline]

def Std.IterM.instForIn' {m : Type w → Type w'} {n : Type w → Type w''} {α β : Type w} [Iterator α m β] [IteratorLoop α m n] [Monad n] [MonadLiftT m n] : ForIn' n (IterM m β) β { mem := fun (it : IterM m β) (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.

instance Std.IterM.instForInOfIteratorLoop {m : Type w → Type w'} {n : Type w → Type w''} {α β : Type w} [Iterator α m β] [IteratorLoop α m n] [MonadLiftT m n] [Monad n] : ForIn n (IterM m β) β

@[inline]

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

Internal implementation detail of the iterator library.

@[inline]

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

Internal implementation detail of the iterator library.

instance Std.IterM.Partial.instForInOfIteratorLoop {m : Type w → Type w'} {n : Type w → Type w''} {α β : Type w} [Iterator α m β] [IteratorLoop α m n] [MonadLiftT m n] [Monad n] : ForIn n (Partial m β) β

instance Std.instForInTotalOfIteratorLoopOfMonadLiftTOfMonadOfFinite {m : Type w → Type w'} {n : Type w → Type w''} {α β : Type w} [Iterator α m β] [IteratorLoop α m n] [MonadLiftT m n] [Monad n] [Iterators.Finite α m] : ForIn n (IterM.Total m β) β

instance Std.IterM.instForMOfIteratorLoop {m : Type w → Type w'} {n : Type w → Type w''} {α β : Type w} [Iterator α m β] [IteratorLoop α m n] [Monad n] [MonadLiftT m n] : ForM n (IterM m β) β

instance Std.IterM.Partial.instForMOfItreratorLoop {m : Type w → Type w'} {n : Type w → Type w''} {α β : Type w} [Monad n] [Iterator α m β] [IteratorLoop α m n] [MonadLiftT m n] : ForM n (Partial m β) β

instance Std.instForMTotalOfIteratorLoopOfMonadOfMonadLiftTOfFinite {m : Type w → Type w'} {n : Type w → Type w''} {α β : Type w} [Iterator α m β] [IteratorLoop α m n] [Monad n] [MonadLiftT m n] [Iterators.Finite α m] : ForM n (IterM.Total m β) β

@[inline]

def Std.IterM.foldM {m : Type w → Type w'} {n : Type w → Type w''} [Monad n] {α β γ : Type w} [Iterator α m β] [IteratorLoop α m n] [MonadLiftT m n] (f : γ → β → n γ) (init : γ) (it : IterM m β) : n γ

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.

The monadic effects of f are interleaved with potential effects caused by the iterator's step function. Therefore, it may not be equivalent to (← it.toList).foldlM.

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

def Std.IterM.Partial.foldM {m n : Type w → Type w'} [Monad n] {α β γ : Type w} [Iterator α m β] [IteratorLoop α m n] [MonadLiftT m n] (f : γ → β → n γ) (init : γ) (it : Partial m β) : n γ

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.

The monadic effects of f are interleaved with potential effects caused by the iterator's step function. Therefore, it may not be equivalent to it.toList.foldlM.

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

@[inline]

def Std.IterM.Total.foldM {m n : Type w → Type w'} [Monad n] {α β γ : Type w} [Iterator α m β] [IteratorLoop α m n] [MonadLiftT m n] [Iterators.Finite α m] (f : γ → β → n γ) (init : γ) (it : Total m β) : n γ

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.

The monadic effects of f are interleaved with potential effects caused by the iterator's step function. Therefore, it may not be 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 IterM.foldM.

@[inline]

def Std.IterM.fold {m : Type w → Type w'} {α β γ : Type w} [Monad m] [Iterator α m β] [IteratorLoop α m m] (f : γ → β → γ) (init : γ) (it : IterM m β) : m γ

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.IterM.Partial.fold (since := "2025-12-04")]

def Std.IterM.Partial.fold {m : Type w → Type w'} {α β γ : Type w} [Monad m] [Iterator α m β] [IteratorLoop α m m] (f : γ → β → γ) (init : γ) (it : Partial m β) : m γ

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.IterM.Total.fold {m : Type w → Type w'} {α β γ : Type w} [Monad m] [Iterator α m β] [IteratorLoop α m m] [Iterators.Finite α m] (f : γ → β → γ) (init : γ) (it : Total m β) : m γ

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 IterM.fold.

@[inline]

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

Iterates over the whole iterator, applying the monadic effects of each step, discarding all emitted values.

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

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

Iterates over the whole iterator, applying the monadic effects of each step, discarding all emitted values.

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

@[inline]

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

Iterates over the whole iterator, applying the monadic effects of each step, discarding all emitted values.

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.drain.

@[specialize #[]]

def Std.IterM.anyM {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [IteratorLoop α m m] (p : β → m (ULift Bool)) (it : IterM m β) : m (ULift Bool)

Returns ULift.up true if the monadic predicate p returns ULift.up true for any element emitted by the iterator it.

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

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

def Std.IterM.Partial.anyM {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [IteratorLoop α m m] (p : β → m (ULift Bool)) (it : Partial m β) : m (ULift Bool)

Returns ULift.up true if the monadic predicate p returns ULift.up true for any element emitted by the iterator it.

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

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

@[inline]

def Std.IterM.Total.anyM {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [IteratorLoop α m m] [Iterators.Finite α m] (p : β → m (ULift Bool)) (it : Total m β) : m (ULift Bool)

Returns ULift.up true if the monadic predicate p returns ULift.up true for any element emitted by the iterator it.

O(|it|). Short-circuits upon encountering the first match. 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 IterM.anyM.

@[inline]

def Std.IterM.any {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [IteratorLoop α m m] (p : β → Bool) (it : IterM m β) : m (ULift Bool)

Returns ULift.up true if the pure predicate p returns true for any element emitted by the iterator it.

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

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

def Std.IterM.Partial.any {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [IteratorLoop α m m] (p : β → Bool) (it : Partial m β) : m (ULift Bool)

Returns ULift.up true if the pure predicate p returns true for any element emitted by the iterator it.

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

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

@[inline]

def Std.IterM.Total.any {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [IteratorLoop α m m] [Iterators.Finite α m] (p : β → Bool) (it : Total m β) : m (ULift Bool)

Returns ULift.up true if the pure predicate p returns true for any element emitted by the iterator it.

O(|it|). Short-circuits upon encountering the first match. 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 IterM.any.

@[specialize #[]]

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

Returns ULift.up true if the monadic predicate p returns ULift.up true for all elements emitted by the iterator it.

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

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

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

Returns ULift.up true if the monadic predicate p returns ULift.up true for all elements emitted by the iterator it.

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

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

@[inline]

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

Returns ULift.up true if the monadic predicate p returns ULift.up true for all elements emitted by the iterator it.

O(|it|). Short-circuits upon encountering the first mismatch. 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 IterM.allM.

@[inline]

def Std.IterM.all {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [IteratorLoop α m m] (p : β → Bool) (it : IterM m β) : m (ULift Bool)

Returns ULift.up true if the pure predicate p returns true for all elements emitted by the iterator it.

O(|it|). Short-circuits upon encountering the first mismatch. 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.toListRev always terminates after finitely many steps.

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

def Std.IterM.Partial.all {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [IteratorLoop α m m] (p : β → Bool) (it : Partial m β) : m (ULift Bool)

Returns ULift.up true if the pure predicate p returns true for all elements emitted by the iterator it.

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

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

@[inline]

def Std.IterM.Total.all {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [IteratorLoop α m m] [Iterators.Finite α m] (p : β → Bool) (it : Total m β) : m (ULift Bool)

Returns ULift.up true if the pure predicate p returns true for all elements emitted by the iterator it.

O(|it|). Short-circuits upon encountering the first mismatch. 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 IterM.all.

@[inline]

def Std.IterM.findSomeM? {α β γ : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [IteratorLoop α m m] (it : IterM m β) (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].iterM IO).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.IterM.findSomeM? (since := "2025-12-04")]

def Std.IterM.Partial.findSomeM? {α β γ : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [IteratorLoop α m m] (it : Partial m β) (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].iterM IO).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.IterM.Total.findSomeM? {α β γ : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [IteratorLoop α m m] [Iterators.Finite α m] (it : Total m β) (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 IterM.findSomeM?.

Example:

#eval ([7, 6, 5, 8, 1, 2, 6].iterM IO).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.IterM.findSome? {α β γ : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [IteratorLoop α m m] (it : IterM m β) (f : β → Option γ) : m (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].iterM Id).findSome? (fun x => if x < 5 then some (10 * x) else none) = pure (some 10)
• ([7, 6, 5, 8, 1, 2, 6].iterM Id).findSome? (fun x => if x < 1 then some (10 * x) else none) = pure none

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

def Std.IterM.Partial.findSome? {α β γ : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [IteratorLoop α m m] (it : Partial m β) (f : β → Option γ) : m (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].iterM Id).allowNontermination.findSome? (fun x => if x < 5 then some (10 * x) else none) = pure (some 10)
• ([7, 6, 5, 8, 1, 2, 6].iterM Id).allowNontermination.findSome? (fun x => if x < 1 then some (10 * x) else none) = pure none

@[inline]

def Std.IterM.Total.findSome? {α β γ : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [IteratorLoop α m m] [Iterators.Finite α m] (it : Partial m β) (f : β → Option γ) : m (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 IterM.findSome?.

Examples:

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

@[inline]

def Std.IterM.findM? {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [IteratorLoop α m m] (it : IterM m β) (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].iterM IO).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.IterM.findM? (since := "2025-12-04")]

def Std.IterM.Partial.findM? {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [IteratorLoop α m m] (it : Partial m β) (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.allowNontermination.findM?, use it.findM?.

Example:

#eval ([7, 6, 5, 8, 1, 2, 6].iterM IO).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.IterM.Total.findM? {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [IteratorLoop α m m] [Iterators.Finite α m] (it : Total m β) (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 IterM.findM?.

Example:

#eval ([7, 6, 5, 8, 1, 2, 6].iterM IO).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.IterM.find? {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [IteratorLoop α m m] (it : IterM m β) (f : β → Bool) : m (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].iterM Id).find? (· < 5) = pure (some 1)
• ([7, 6, 5, 8, 1, 2, 6].iterM Id).find? (· < 1) = pure none

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

def Std.IterM.Partial.find? {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [IteratorLoop α m m] (it : Partial m β) (f : β → Bool) : m (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].iterM Id).allowNontermination.find? (· < 5) = pure (some 1)
• ([7, 6, 5, 8, 1, 2, 6].iterM Id).allowNontermination.find? (· < 1) = pure none

@[inline]

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

Examples:

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

@[inline]

def Std.IterM.count {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] [IteratorLoop α m m] [Monad m] (it : IterM m β) : m (ULift 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.IterM.count (since := "2025-10-29")]

def Std.IterM.size {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] [IteratorLoop α m m] [Monad m] (it : IterM m β) : m (ULift 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.IterM.count (since := "2025-12-04")]

def Std.IterM.Partial.count {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] [IteratorLoop α m m] [Monad m] (it : Partial m β) : m (ULift 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.IterM.Partial.count (since := "2025-10-29")]

def Std.IterM.Partial.size {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] [IteratorLoop α m m] [Monad m] (it : Partial m β) : m (ULift 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.