22.3. 使用迭代器🔗

使用迭代器的主要方式有以下三种：

将其转换为顺序数据结构: 函数 Iter.toList、Iter.toArray 及其一元等效函数 IterM.toList 和 IterM.toArray 按顺序构造包含迭代器中的值的列表或数组。只有有限迭代器可以转换为顺序数据结构。
Lean.Parser.Term.doFor : doElem`for x in e do s` iterates over `e` assuming `e`'s type has an instance of the `ForIn` typeclass. `break` and `continue` are supported inside `for` loops. `for x in e, x2 in e2, ... do s` iterates of the given collections in parallel, until at least one of them is exhausted. The types of `e2` etc. must implement the `Std.ToStream` typeclass.for 循环: Lean.Parser.Term.doFor : doElem`for x in e do s` iterates over `e` assuming `e`'s type has an instance of the `ForIn` typeclass. `break` and `continue` are supported inside `for` loops. `for x in e, x2 in e2, ... do s` iterates of the given collections in parallel, until at least one of them is exhausted. The types of `e2` etc. must implement the `Std.ToStream` typeclass.for 循环可以使用迭代器，使每个值在其主体中可用。这要求迭代器具有循环 monad 的 IteratorLoop 实例。
单步执行迭代器: 迭代器可以一一提供它们的值，客户端代码依次显式请求每个新值。当单步执行时，迭代器仅执行足够的计算来产生所请求的值。

Converting Iterators to Lists

在 countdown 中，使用 Iter.map 将范围上的迭代器转换为字符串上的迭代器。对 Iter.map 的调用不会导致对该范围进行任何迭代，直到调用 Iter.toList，此时该范围的每个元素都会生成并转换为字符串。

def countdown : String :=
  let steps : Iter String := (0...10).iter.map (s!"{10 - ·}!\n")
  String.join steps.toList

10!
9!
8!
7!
6!
5!
4!
3!
2!
1!

#eval IO.println countdown

10!
9!
8!
7!
6!
5!
4!
3!
2!
1!

Live ↪

Converting Infinite Iterators to Lists

尝试从迭代器构建所有自然数的列表将产生无限循环：

def allNats : List Nat :=
  let steps : Iter Nat := (0...*).iter
  steps.toList

组合器 Iter.ensureTermination 产生一个排除非终止的迭代器。这些迭代器保证在有限多个步骤后终止，因此当 Lean 无法证明迭代器有限时不能使用。

def allNats : List Nat :=
  let steps := (0...*).iter.ensureTermination
  failed to synthesize instance of type class
  Finite (Rxi.Iterator Nat) Id

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.steps.toList

生成的错误消息指出不存在 Finite 实例：

failed to synthesize instance of type class
  Finite (Rxi.Iterator Nat) Id

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.

Live ↪

Consuming Iterators in Loops

该程序创建一个范围内的字符串迭代器，然后在 Lean.Parser.Term.doFor : doElem`for x in e do s` iterates over `e` assuming `e`'s type has an instance of the `ForIn` typeclass. `break` and `continue` are supported inside `for` loops. `for x in e, x2 in e2, ... do s` iterates of the given collections in parallel, until at least one of them is exhausted. The types of `e2` etc. must implement the `Std.ToStream` typeclass.for 循环中使用这些字符串：

def countdown (n : Nat) : IO Unit := do
  let steps : Iter String := (0...n).iter.map (s!"{n - ·}!")
  for i in steps do
    IO.println i
  IO.println "Blastoff!"

5!
4!
3!
2!
1!
Blastoff!
#eval countdown 5

5!
4!
3!
2!
1!
Blastoff!

Live ↪

Consuming Iterators Directly

函数 countdown 直接调用范围迭代器的 step 函数，处理三种可能情况中的每一种。

def countdown (n : Nat) : IO Unit := do
  let steps : Iter Nat := (0...n).iter
  go steps
where
  go iter := do
    match iter.step with
    | .done _ => pure ()
    | .skip iter' _ => go iter'
    | .yield iter' i _ => do
      IO.println s!"{i}!"
      if i == 2 then
        IO.println s!"Almost there..."
      go iter'
  termination_by iter.finitelyManySteps

Live ↪

22.3.1. 步进迭代器🔗

使用 Iter.step 或 IterM.step 手动步进迭代器。

def

Std.Iter.step.{w} {α β : Type w} [Iterator α Id β] (it : Iter β) :
  it.Step
Std.Iter.step.{w} {α β : Type w}
  [Iterator α Id β] (it : Iter β) :
  it.Step

Makes a single step with the given iterator it, potentially emitting a value and providing a succeeding iterator. If this function is used recursively, termination can sometimes be proved with the termination measures it.finitelyManySteps and it.finitelyManySkips.

def

Std.IterM.step.{w, w'} {α : Type w} {m : Type w → Type w'} {β : Type w}
  [Iterator α m β] (it : IterM m β) : m (Std.Shrink it.Step)
Std.IterM.step.{w, w'} {α : Type w}
  {m : Type w → Type w'} {β : Type w}
  [Iterator α m β] (it : IterM m β) :
  m (Std.Shrink it.Step)

22.3.1.1. 终止🔗

当手动步进有限迭代器时，终止测量 finitelyManySteps 和 finitelyManySkips 可用于表示每一步都使迭代更接近结束。良基递归的证明自动化已预先配置，以证明步骤后的递归调用会减少这些措施。

Finitely Many Skips

此函数返回迭代器的第一个元素（如果有），否则返回 none。由于迭代器必须高效，因此保证最多在有限数量的 skip 之后返回一个元素。即使对于无限迭代器，该函数也会终止。

def getFirst {α β} [Iterator α Id β] [Productive α Id]
    (it : @Iter α β) : Option β :=
  match it.step with
  | .done .. => none
  | .skip it' .. => getFirst it'
  | .yield _ x .. => pure x
termination_by it.finitelyManySkips

Live ↪

def

Std.Iter.finitelyManySteps.{w} {α β : Type w} [Iterator α Id β]
  [Finite α Id] (it : Iter β) : IterM.TerminationMeasures.Finite α Id
Std.Iter.finitelyManySteps.{w}
  {α β : Type w} [Iterator α Id β]
  [Finite α Id] (it : Iter β) :
  IterM.TerminationMeasures.Finite α Id

Termination measure to be used in well-founded recursive functions recursing over a finite iterator (see also Finite).

def

Std.IterM.finitelyManySteps.{w, w'} {α : Type w} {m : Type w → Type w'}
  {β : Type w} [Iterator α m β] [Finite α m] (it : IterM m β) :
  IterM.TerminationMeasures.Finite α m
Std.IterM.finitelyManySteps.{w, w'}
  {α : Type w} {m : Type w → Type w'}
  {β : Type w} [Iterator α m β]
  [Finite α m] (it : IterM m β) :
  IterM.TerminationMeasures.Finite α m

Termination measure to be used in well-founded recursive functions recursing over a finite iterator (see also Finite).

structure

Std.IterM.TerminationMeasures.Finite.{w, w'} (α : Type w)
  (m : Type w → Type w') {β : Type w} [Iterator α m β] : Type w
Std.IterM.TerminationMeasures.Finite.{w,
    w'}
  (α : Type w) (m : Type w → Type w')
  {β : Type w} [Iterator α m β] : Type w

This type is a wrapper around IterM so that it becomes a useful termination measure for recursion over finite iterators. See also IterM.finitelyManySteps and Iter.finitelyManySteps.

Constructor

Std.IterM.TerminationMeasures.Finite.mk.{w, w'}

Fields

it : IterM m β

The wrapped iterator.

In the wrapper, its finiteness is used as a termination measure.

def

Std.Iter.finitelyManySkips.{w} {α β : Type w} [Iterator α Id β]
  [Productive α Id] (it : Iter β) :
  IterM.TerminationMeasures.Productive α Id
Std.Iter.finitelyManySkips.{w}
  {α β : Type w} [Iterator α Id β]
  [Productive α Id] (it : Iter β) :
  IterM.TerminationMeasures.Productive α
    Id

Termination measure to be used in well-founded recursive functions recursing over a productive iterator (see also Productive).

def

Std.IterM.finitelyManySkips.{w, w'} {α : Type w} {m : Type w → Type w'}
  {β : Type w} [Iterator α m β] [Productive α m] (it : IterM m β) :
  IterM.TerminationMeasures.Productive α m
Std.IterM.finitelyManySkips.{w, w'}
  {α : Type w} {m : Type w → Type w'}
  {β : Type w} [Iterator α m β]
  [Productive α m] (it : IterM m β) :
  IterM.TerminationMeasures.Productive α m

Termination measure to be used in well-founded recursive functions recursing over a productive iterator (see also Productive).

structure

Std.IterM.TerminationMeasures.Productive.{w, w'} (α : Type w)
  (m : Type w → Type w') {β : Type w} [Iterator α m β] : Type w
Std.IterM.TerminationMeasures.Productive.{w,
    w'}
  (α : Type w) (m : Type w → Type w')
  {β : Type w} [Iterator α m β] : Type w

This type is a wrapper around IterM so that it becomes a useful termination measure for recursion over productive iterators. See also IterM.finitelyManySkips and Iter.finitelyManySkips.

Constructor

Std.IterM.TerminationMeasures.Productive.mk.{w, w'}

Fields

it : IterM m β

The wrapped iterator.

In the wrapper, its productivity is used as a termination measure.

22.3.2. 使用纯迭代器🔗

def

Std.Iter.fold.{w, x} {α β : Type w} {γ : Type x} [Iterator α Id β]
  [IteratorLoop α Id Id] (f : γ → β → γ) (init : γ) (it : Iter β) : γ
Std.Iter.fold.{w, x} {α β : 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.

def

Std.Iter.foldM.{x, x', w} {m : Type x → Type x'} [Monad m]
  {α β : Type w} {γ : Type x} [Iterator α Id β] [IteratorLoop α Id m]
  (f : γ → β → m γ) (init : γ) (it : Iter β) : m γ
Std.Iter.foldM.{x, x', w}
  {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.

def

Std.Iter.length.{w} {α β : Type w} [Iterator α Id β]
  [IteratorLoop α Id Id] (it : Iter β) : Nat
Std.Iter.length.{w} {α β : 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.

def

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

def

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

def

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

def

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

def

Std.Iter.find?.{w} {α β : Type w} [Iterator α Id β]
  [IteratorLoop α Id Id] (it : Iter β) (f : β → Bool) : Option β
Std.Iter.find?.{w} {α β : 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

def

Std.Iter.findM?.{w, w'} {α β : Type w} {m : Type w → Type w'} [Monad m]
  [Iterator α Id β] [IteratorLoop α Id m] (it : Iter β)
  (f : β → m (ULift Bool)) : m (Option β)
Std.Iter.findM?.{w, w'} {α β : 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

def

Std.Iter.findSome?.{w, x} {α β : Type w} {γ : Type x} [Iterator α Id β]
  [IteratorLoop α Id Id] (it : Iter β) (f : β → Option γ) : Option γ
Std.Iter.findSome?.{w, x} {α β : 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

def

Std.Iter.findSomeM?.{w, x, w'} {α β : Type w} {γ : Type x}
  {m : Type x → Type w'} [Monad m] [Iterator α Id β]
  [IteratorLoop α Id m] (it : Iter β) (f : β → m (Option γ)) :
  m (Option γ)
Std.Iter.findSomeM?.{w, x, w'}
  {α β : 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:

some 10Almost! 6
Almost! 5
#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

def

Std.Iter.atIdx?.{u_1} {α β : Type u_1} [Iterator α Id β]
  [IteratorAccess α Id] (n : Nat) (it : Iter β) : Option β
Std.Iter.atIdx?.{u_1} {α β : Type u_1}
  [Iterator α Id β] [IteratorAccess α Id]
  (n : Nat) (it : Iter β) : Option β

Returns the n-th value emitted by it, or none if it terminates earlier.

For monadic iterators, the monadic effects of this operation may differ from manually iterating to the n-th value because atIdx? can take shortcuts. By the signature, the return value is guaranteed to plausible in the sense of IterM.IsPlausibleNthOutputStep.

This function is only available for iterators that explicitly support it by implementing the IteratorAccess typeclass.

def

Std.Iter.atIdxSlow?.{u_1} {α β : Type u_1} [Iterator α Id β] (n : Nat)
  (it : Iter β) : Option β
Std.Iter.atIdxSlow?.{u_1} {α β : Type u_1}
  [Iterator α Id β] (n : Nat)
  (it : Iter β) : Option β

If possible, takes n steps with the iterator it and returns the n-th emitted value, or none if it finished before emitting n values.

If the iterator is not productive, this function might run forever in an endless loop of iterator steps. The variant it.ensureTermination.atIdxSlow? is guaranteed to terminate after finitely many steps.

22.3.3. 使用 Monadic 迭代器🔗

def

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

def

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

def

Std.IterM.foldM.{w, w', w''} {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 γ
Std.IterM.foldM.{w, w', w''}
  {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.

def

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

def

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

def

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

def

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

def

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

def

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

def

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

def

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

def

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

some 10Almost! 6
Almost! 5
#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

def

Std.IterM.atIdx?.{u_1, u_2} {α : Type u_1} {m : Type u_1 → Type u_2}
  {β : Type u_1} [Iterator α m β] [IteratorAccess α m] [Monad m]
  (it : IterM m β) (n : Nat) : m (Option β)
Std.IterM.atIdx?.{u_1, u_2} {α : Type u_1}
  {m : Type u_1 → Type u_2} {β : Type u_1}
  [Iterator α m β] [IteratorAccess α m]
  [Monad m] (it : IterM m β) (n : Nat) :
  m (Option β)

Returns the n-th value emitted by it, or none if it terminates earlier.

This function is only available for iterators that explicitly support it by implementing the IteratorAccess typeclass.

22.3.4. 收藏家🔗

收集器使用迭代器，返回列表或数组中的所有数据。为了被收集，迭代器必须是有限的。

def

Std.Iter.toArray.{w} {α β : Type w} [Iterator α Id β] (it : Iter β) :
  Array β
Std.Iter.toArray.{w} {α β : Type w}
  [Iterator α Id β] (it : Iter β) :
  Array β

Traverses the given iterator and stores the emitted values in an array.

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

def

Std.IterM.toArray.{w, w'} {α β : Type w} {m : Type w → Type w'}
  [Monad m] [Iterator α m β] (it : IterM m β) : m (Array β)
Std.IterM.toArray.{w, w'} {α β : Type w}
  {m : Type w → Type w'} [Monad m]
  [Iterator α m β] (it : IterM m β) :
  m (Array β)

Traverses the given iterator and stores the emitted values in an array.

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

def

Std.Iter.toList.{w} {α β : Type w} [Iterator α Id β] (it : Iter β) :
  List β
Std.Iter.toList.{w} {α β : Type w}
  [Iterator α Id β] (it : Iter β) : List β

Traverses the given iterator and stores the emitted values in a list. Because lists are prepend-only, toListRev is usually more efficient that toList.

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

def

Std.IterM.toList.{w, w'} {α : Type w} {m : Type w → Type w'} [Monad m]
  {β : Type w} [Iterator α m β] (it : IterM m β) : m (List β)
Std.IterM.toList.{w, w'} {α : Type w}
  {m : Type w → Type w'} [Monad m]
  {β : Type w} [Iterator α m β]
  (it : IterM m β) : m (List β)

Traverses the given iterator and stores the emitted values in a list. Because lists are prepend-only, toListRev is usually more efficient that toList.

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

def

Std.Iter.toListRev.{w} {α β : Type w} [Iterator α Id β] (it : Iter β) :
  List β
Std.Iter.toListRev.{w} {α β : Type w}
  [Iterator α Id β] (it : Iter β) : List β

Traverses the given iterator and stores the emitted values in reverse order in a list. Because lists are prepend-only, this toListRev is usually more efficient that toList.

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

def

Std.IterM.toListRev.{w, w'} {α : Type w} {m : Type w → Type w'}
  [Monad m] {β : Type w} [Iterator α m β] (it : IterM m β) : m (List β)
Std.IterM.toListRev.{w, w'} {α : Type w}
  {m : Type w → Type w'} [Monad m]
  {β : Type w} [Iterator α m β]
  (it : IterM m β) : m (List β)

Traverses the given iterator and stores the emitted values in reverse order in a list. Because lists are prepend-only, this toListRev is usually more efficient that toList.

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