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 and IteratorLoopPartial typeclasses. 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.Iterators.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.

Equations

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

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

Equations

• Std.Iterators.IteratorLoop.WellFounded α m plausible_forInStep = WellFounded (Std.Iterators.IteratorLoop.rel α m plausible_forInStep)

class Std.Iterators.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 with the complication that it can be used for infinite iterators, too -- given a proof that the given loop will nevertheless terminate.

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) : WellFounded α m plausible_forInStep → (it : IterM m β) → γ → ((b : β) → it.IsPlausibleIndirectOutput b → (c : γ) → n (Subtype (plausible_forInStep b c))) → n γ

theorem Std.Iterators.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

theorem Std.Iterators.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

class Std.Iterators.IteratorLoopPartial (α : 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')

IteratorLoopPartial α m provides efficient implementations of loop-based consumers for α-based iterators. The basis is a partial, i.e. potentially nonterminating, ForIn instance.

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.

• forInPartial (_liftBind : (γ : Type w) → (δ : Type x) → (γ → n δ) → m γ → n δ) {γ : Type x} (it : IterM m β) : γ → ((b : β) → it.IsPlausibleIndirectOutput b → γ → n (ForInStep γ)) → n γ

structure Std.Iterators.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 β
• acc : γ

instance Std.Iterators.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)

Equations

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

@[irreducible, specialize #[]]

def Std.Iterators.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) (plausible_forInStep : β → γ → ForInStep γ → Prop) (wf : IteratorLoop.WellFounded α m plausible_forInStep) (it : IterM m β) (init : γ) (P : β → Prop) (hP : ∀ (b : β), it.IsPlausibleIndirectOutput b → P b) (f : (b : β) → P b → (c : γ) → n (Subtype (plausible_forInStep b c))) : n γ

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

Equations

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

@[irreducible]

theorem Std.Iterators.IterM.DefaultConsumers.forIn'_eq_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} {Pl : β → γ → ForInStep γ → Prop} {wf : IteratorLoop.WellFounded α m Pl} {it : IterM m β} {init : γ} {P : β → Prop} {hP : ∀ (b : β), it.IsPlausibleIndirectOutput b → P b} {Q : β → Prop} {hQ : ∀ (b : β), it.IsPlausibleIndirectOutput b → Q b} {f : (b : β) → P b → (c : γ) → n (Subtype (Pl b c))} {g : (b : β) → Q b → (c : γ) → n (Subtype (Pl b c))} (hfg : ∀ (b : β) (c : γ) (hPb : P b) (hQb : Q b), f b hPb c = g b hQb c) : forIn' lift γ Pl wf it init P hP f = forIn' lift γ Pl wf it init Q hQ g

@[inline]

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

Equations

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

class Std.Iterators.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] : IteratorLoop.forIn lift = IteratorLoop.forIn lift

@[specialize #[]]

partial def Std.Iterators.IterM.DefaultConsumers.forInPartial {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) (it : IterM m β) (init : γ) (f : (b : β) → it.IsPlausibleIndirectOutput b → γ → n (ForInStep γ)) : n γ

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

@[inline]

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

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

Equations

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

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

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

@[inline]

def Std.Iterators.IteratorLoop.finiteForIn' {m : Type w → Type w'} {n : Type x → Type x'} {α β : Type w} [Iterator α m β] [Finite α m] [IteratorLoop α m 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.

Equations

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

@[inline]

def Std.Iterators.IterM.instForIn' {m : Type w → Type w'} {n : Type w → Type w''} {α β : Type w} [Iterator α m β] [Finite α 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.

Equations

• Std.Iterators.IterM.instForIn' = Std.Iterators.IteratorLoop.finiteForIn' fun (x x_1 : Type ?u.76) (f : x → n x_1) (x_2 : m x) => monadLift x_2 >>= f

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

Equations

• Std.Iterators.instForInIterMOfFiniteOfIteratorLoopOfMonadLiftTOfMonad = instForInOfForIn'

@[inline]

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

Equations

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

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

Equations

• Std.Iterators.instForInPartialOfIteratorLoopPartialOfMonadLiftTOfMonad = instForInOfForIn'

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

Equations

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

instance Std.Iterators.instForMPartialOfIteratorLoopPartialOfMonadLiftT {m : Type w → Type w'} {n : Type w → Type w''} {α β : Type w} [Iterator α m β] [IteratorLoopPartial α m n] [MonadLiftT m n] : ForM n (IterM.Partial m β) β

Equations

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

@[inline]

def Std.Iterators.IterM.foldM {m : Type w → Type w'} {n : Type w → Type w''} [Monad n] {α β γ : Type w} [Iterator α m β] [Finite α 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.

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.IterM.foldM f init it = forIn it init fun (x : β) (acc : γ) => ForInStep.yield <$> f acc x

@[inline]

def Std.Iterators.IterM.Partial.foldM {m n : Type w → Type w'} [Monad n] {α β γ : Type w} [Iterator α m β] [IteratorLoopPartial α 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 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.IterM.Partial.foldM f init it = forIn it init fun (x : β) (acc : γ) => ForInStep.yield <$> f acc x

@[inline]

def Std.Iterators.IterM.fold {m : Type w → Type w'} {α β γ : Type w} [Monad m] [Iterator α m β] [Finite α 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.

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.IterM.fold f init it = forIn it init fun (x : β) (acc : γ) => pure (ForInStep.yield (f acc x))

@[inline]

def Std.Iterators.IterM.Partial.fold {m : Type w → Type w'} {α β γ : Type w} [Monad m] [Iterator α m β] [IteratorLoopPartial α 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 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.IterM.Partial.fold f init it = forIn it init fun (x : β) (acc : γ) => pure (ForInStep.yield (f acc x))

@[inline]

def Std.Iterators.IterM.drain {α : Type w} {m : Type w → Type w'} [Monad m] {β : Type w} [Iterator α m β] [Finite α 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.

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.drain instead of it.drain. However, it is not possible to formally verify the behavior of the partial variant.

Equations

• it.drain = Std.Iterators.IterM.fold (fun (x : PUnit) (x_1 : β) => PUnit.unit) PUnit.unit it

@[inline]

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

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

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

Equations

• it.drain = Std.Iterators.IterM.Partial.fold (fun (x : PUnit) (x_1 : β) => PUnit.unit) PUnit.unit it

@[specialize #[]]

def Std.Iterators.IterM.anyM {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [IteratorLoop α m m] [Finite α 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(|xs|). Short-circuits upon encountering the first match. The elements in it are examined in order of iteration.

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.anyM instead of it.anyM. However, it is not possible to formally verify the behavior of the partial variant.

Equations

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

@[specialize #[]]

def Std.Iterators.IterM.Partial.anyM {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [IteratorLoopPartial α 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(|xs|). Short-circuits upon encountering the first match. The elements in it are examined in order of iteration.

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

Equations

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

@[inline]

def Std.Iterators.IterM.any {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [IteratorLoop α m m] [Finite α 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(|xs|). Short-circuits upon encountering the first match. The elements in it are examined in order of iteration.

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.any instead of it.any. However, it is not possible to formally verify the behavior of the partial variant.

Equations

• Std.Iterators.IterM.any p it = Std.Iterators.IterM.anyM (fun (x : β) => pure { down := p x }) it

@[inline]

def Std.Iterators.IterM.Partial.any {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [IteratorLoopPartial α 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(|xs|). Short-circuits upon encountering the first match. The elements in it are examined in order of iteration.

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

Equations

• Std.Iterators.IterM.Partial.any p it = Std.Iterators.IterM.Partial.anyM (fun (x : β) => pure { down := p x }) it

@[specialize #[]]

def Std.Iterators.IterM.allM {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [IteratorLoop α m m] [Finite α 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(|xs|). Short-circuits upon encountering the first mismatch. The elements in it are examined in order of iteration.

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.allM instead of it.allM. However, it is not possible to formally verify the behavior of the partial variant.

Equations

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

@[specialize #[]]

def Std.Iterators.IterM.Partial.allM {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [IteratorLoopPartial α 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(|xs|). Short-circuits upon encountering the first mismatch. The elements in it are examined in order of iteration.

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

Equations

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

@[inline]

def Std.Iterators.IterM.all {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [IteratorLoop α m m] [Finite α 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(|xs|). Short-circuits upon encountering the first mismatch. The elements in it are examined in order of iteration.

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.all instead of it.all. However, it is not possible to formally verify the behavior of the partial variant.

Equations

• Std.Iterators.IterM.all p it = Std.Iterators.IterM.allM (fun (x : β) => pure { down := p x }) it

@[inline]

def Std.Iterators.IterM.Partial.all {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [IteratorLoopPartial α 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(|xs|). Short-circuits upon encountering the first mismatch. The elements in it are examined in order of iteration.

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

Equations

• Std.Iterators.IterM.Partial.all p it = Std.Iterators.IterM.Partial.allM (fun (x : β) => pure { down := p x }) it

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

def Std.Iterators.IterM.findSome? {α β γ : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [IteratorLoop α m m] [Finite α m] (it : IterM m β) (f : β → Option γ) : m (Option γ)

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

def Std.Iterators.IterM.count {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] [Finite α 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.

Equations

• it.count = Std.Iterators.IterM.fold (fun (acc : ULift Nat) (x : β) => { down := acc.down + 1 }) { down := 0 } it

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

def Std.Iterators.IterM.size {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] [Finite α 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.

Equations

• it.size = it.count

@[inline]

def Std.Iterators.IterM.Partial.count {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] [IteratorLoopPartial α 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.

Equations

• it.count = Std.Iterators.IterM.Partial.fold (fun (acc : ULift Nat) (x : β) => { down := acc.down + 1 }) { down := 0 } it

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

def Std.Iterators.IterM.Partial.size {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] [IteratorLoopPartial α 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.

Equations

• it.size = it.count