22.3. 消费迭代器🔗

消费迭代器主要有三种方式：

将其转换为顺序数据结构: 函数 Iter.toList、Iter.toArray 及其单子式对应项 IterM.toList 和 IterM.toArray，会构造按顺序包含迭代器各值的列表或数组。只有有限迭代器才能转换为顺序数据结构。
Lean.Parser.Term.doFor : doElemfor 循环: Lean.Parser.Term.doFor : doElemfor 循环可以消费迭代器，让每个值在循环体中可用。这要求迭代器具有针对该循环所用单子的 IteratorLoop 实例。
逐步推进迭代器: 迭代器可以逐个提供其值，由客户端代码依次显式请求每个新值。逐步推进时，迭代器只执行足以产出所请求值的计算。

将迭代器转换为列表

在 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!

在线查看 ↪

将无限迭代器转换为列表

尝试从迭代器构造包含所有自然数的列表会产生无限循环：

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.

在线查看 ↪

在循环中消费迭代器

该程序从区间创建一个字符串迭代器，然后在 Lean.Parser.Term.doFor : doElemfor 循环中消费这些字符串：

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!

在线查看 ↪

直接消费迭代器

函数 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

在线查看 ↪

22.3.1. 逐步推进迭代器🔗

可以使用 Iter.step 或 IterM.step 手动推进迭代器。

定义

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

让给定迭代器 it 执行一步；这一步可能发出一个值，并提供后继迭代器。若递归使用此函数，有时可用终止度量 it.finitelyManySteps 和 it.finitelyManySkips 证明终止。

定义

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 表明每一步都让迭代更接近结束。良基递归的证明自动化已预先配置，可证明步骤之后的递归调用会减小这些度量。

有限次跳过

该函数在迭代器存在首个元素时返回它，否则返回 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

在线查看 ↪

定义

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

在对有限迭代器进行良基递归的函数中使用的终止度量（另见 Finite）。

定义

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

在对有限迭代器进行良基递归的函数中使用的终止度量（另见 Finite）。

结构体

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

此类型包装 IterM，使其可用作有限迭代器递归的终止度量。另见 IterM.finitelyManySteps 和 Iter.finitelyManySteps。

构造子

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

字段

it : IterM m β

被包装的迭代器。

在此包装中，它的有限性被用作终止度量。

定义

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

在对能产迭代器进行良基递归的函数中使用的终止度量（另见 Productive）。

定义

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

在对能产迭代器进行良基递归的函数中使用的终止度量（另见 Productive）。

结构体

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

此类型包装 IterM，使其可用作能产迭代器递归的终止度量。另见 IterM.finitelyManySkips 和 Iter.finitelyManySkips。

构造子

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

字段

it : IterM m β

被包装的迭代器。

在此包装中，它的能产性被用作终止度量。

22.3.2. 消费纯迭代器🔗

定义

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 β) : γ

从左侧用函数折叠迭代器，从 init 开始累积值。按顺序使用 f 将累积值与列表中的每个元素结合。

它等价于 it.toList.foldl。

定义

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 γ

从左侧用单子式函数折叠迭代器，从 init 开始累积值。按顺序使用 f 将累积值与列表中的每个元素结合。

它等价于 it.toList.foldlM。

定义

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

逐步遍历整个迭代器，并统计发出的输出数。

性能：

此函数的运行时间与迭代器执行的步骤数呈线性关系。

定义

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

若纯谓词 p 对迭代器 it 发出的任一元素返回 true，则返回 true。

O(|xs|)。遇到第一个匹配项即短路。按迭代顺序检查 it 中的元素。

定义

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

若单子式谓词 p 对迭代器 it 发出的任一元素返回 true，则返回 true。

O(|xs|)。遇到第一个匹配项即短路。按迭代顺序检查 it 中的元素。

定义

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

若纯谓词 p 对迭代器 it 发出的所有元素返回 true，则返回 true。

O(|xs|)。遇到第一个不匹配项即短路。按迭代顺序检查 it 中的元素。

定义

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

若单子式谓词 p 对迭代器 it 发出的所有元素返回 true，则返回 true。

O(|xs|)。遇到第一个不匹配项即短路。按迭代顺序检查 it 中的元素。

定义

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 β

返回迭代器中第一个使谓词 p 返回 true 的输出；若找不到这样的输出，则返回 none。

O(|it|)。遇到第一个匹配项即短路。按迭代顺序检查 it 中的元素。

若迭代器不是有限的，此函数可能永远运行。变体 it.ensureTermination.find? 总会在有限步后终止。

示例：

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

定义

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 β)

返回迭代器中第一个使单子式谓词 p 返回 true 的输出；若找不到这样的元素，则返回 none。

O(|it|)。当 f 返回 true 时短路。按迭代顺序检查 it 的输出。

若迭代器不是有限的，此函数可能永远运行。变体 it.ensureTermination.findM? 总会在有限步后终止。

示例：

#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

定义

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 γ

按顺序将 f 应用于迭代器的每个输出，并返回第一个非 none 的结果。若 f 对所有输出都返回 none，则返回 none。

O(|it|)。当 f 返回 some _ 时短路。按迭代顺序检查 it 的输出。

若迭代器不是有限的，此函数可能永远运行。变体 it.ensureTermination.findSome? 总会在有限步后终止。

示例：

[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

定义

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 γ)

按顺序将单子式函数 f 应用于迭代器的每个输出，并返回第一个非 none 的结果。若 f 对所有输出都返回 none，则返回 none。

O(|it|)。当 f 返回 some _ 时短路。按迭代顺序检查 it 的输出。

若迭代器不是有限的，此函数可能永远运行。变体 it.ensureTermination.findSomeM? 总会在有限步后终止。

示例：

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

定义

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 β

返回 it 发出的第 n 个值；若 it 更早终止，则返回 none。

对于单子式迭代器，由于 atIdx? 可以走捷径，此操作的单子式效应可能不同于手动迭代到第 n 个值。由签名保证，返回值在 IterM.IsPlausibleNthOutputStep 的意义下是合理的。

此函数仅适用于通过实现 IteratorAccess 类型类而显式支持它的迭代器。

定义

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 β

若可能，令迭代器 it 执行 n 步，并返回发出的第 n 个值；若 it 在发出 n 个值之前结束，则返回 none。

若迭代器不能产，此函数可能陷入无休止的迭代步骤循环。变体 it.ensureTermination.atIdxSlow? 保证在有限步后终止。

22.3.3. 消费单子式迭代器🔗

定义

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

遍历整个迭代器，执行每一步的单子式效应，并丢弃所有发出的值。

定义

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 γ

从左侧用函数折叠迭代器，从 init 开始累积值。按顺序使用 f 将累积值与列表中的每个元素结合。

它等价于 it.toList.foldl。

定义

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 γ

从左侧用单子式函数折叠迭代器，从 init 开始累积值。按顺序使用 f 将累积值与列表中的每个元素结合。

f 的单子式效应与迭代器步进函数可能产生的效应交错。因此，它不一定等价于 (← it.toList).foldlM。

定义

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)

逐步遍历整个迭代器，并统计发出的输出数。

性能：

此函数的运行时间与迭代器执行的步骤数呈线性关系。

定义

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)

若纯谓词 p 对迭代器 it 发出的任一元素返回 true，则返回 ULift.up true。

O(|it|)。遇到第一个匹配项即短路。按迭代顺序检查 it 的输出。

定义

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)

若单子式谓词 p 对迭代器 it 发出的任一元素返回 ULift.up true，则返回 ULift.up true。

O(|it|)。遇到第一个匹配项即短路。按迭代顺序检查 it 中的元素。

定义

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)

若纯谓词 p 对迭代器 it 发出的所有元素返回 true，则返回 ULift.up true。

O(|it|)。遇到第一个不匹配项即短路。按迭代顺序检查 it 中的元素。

若迭代器不是有限的，此函数可能永远运行。变体 it.ensureTermination.toListRev 总会在有限步后终止。

定义

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)

若单子式谓词 p 对迭代器 it 发出的所有元素返回 ULift.up true，则返回 ULift.up true。

O(|it|)。遇到第一个不匹配项即短路。按迭代顺序检查 it 中的元素。

定义

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 β)

返回迭代器中第一个使谓词 p 返回 true 的输出；若找不到这样的输出，则返回 none。

O(|it|)。遇到第一个匹配项即短路。按迭代顺序检查 it 中的元素。

若迭代器不是有限的，此函数可能永远运行。变体 it.ensureTermination.find? 总会在有限步后终止。

示例：

([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

定义

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 β)

返回迭代器中第一个使单子式谓词 p 返回 true 的输出；若找不到这样的元素，则返回 none。

O(|it|)。当 f 返回 true 时短路。按迭代顺序检查 it 的输出。

若迭代器不是有限的，此函数可能永远运行。变体 it.ensureTermination.findM? 总会在有限步后终止。

示例：

#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

定义

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 γ)

按顺序将 f 应用于迭代器的每个输出，并返回第一个非 none 的结果。若 f 对所有输出都返回 none，则返回 none。

O(|it|)。当 f 返回 some _ 时短路。按迭代顺序检查 it 的输出。

若迭代器不是有限的，此函数可能永远运行。变体 it.ensureTermination.findSome? 总会在有限步后终止。

示例：

([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

定义

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 γ)

按顺序将单子式函数 f 应用于迭代器的每个输出，并返回第一个非 none 的结果。若 f 对所有输出都返回 none，则返回 none。

O(|it|)。当 f 返回 some _ 时短路。按迭代顺序检查 it 的输出。

若迭代器不是有限的，此函数可能永远运行。变体 it.ensureTermination.findSomeM? 总会在有限步后终止。

示例：

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

定义

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 β)

返回 it 发出的第 n 个值；若 it 更早终止，则返回 none。

此函数仅适用于通过实现 IteratorAccess 类型类而显式支持它的迭代器。

22.3.4. 收集器🔗

收集器消费迭代器，并以列表或数组返回其全部数据。可被收集的迭代器必须是有限的。

定义

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

遍历给定迭代器，并把发出的值存入数组。

若迭代器不是有限的，此函数可能永远运行。变体 it.ensureTermination.toArray 总会在有限步后终止。

定义

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 β)

遍历给定迭代器，并把发出的值存入数组。

若迭代器不是有限的，此函数可能永远运行。变体 it.ensureTermination.toArray 总会在有限步后终止。

定义

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

遍历给定迭代器，并把发出的值存入列表。由于列表只能在头部添加元素，toListRev 通常比 toList 更高效。

若迭代器不是有限的，此函数可能永远运行。变体 it.ensureTermination.toList 总会在有限步后终止。

定义

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 β)

遍历给定迭代器，并把发出的值存入列表。由于列表只能在头部添加元素，toListRev 通常比 toList 更高效。

若迭代器不是有限的，此函数可能永远运行。变体 it.ensureTermination.toList 总会在有限步后终止。

定义

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

遍历给定迭代器，并按逆序把发出的值存入列表。由于列表只能在头部添加元素，toListRev 通常比 toList 更高效。

若迭代器不是有限的，此函数可能永远运行。变体 it.ensureTermination.toListRev 总会在有限步后终止。

定义

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 β)

遍历给定迭代器，并按逆序把发出的值存入列表。由于列表只能在头部添加元素，toListRev 通常比 toList 更高效。

若迭代器不是有限的，此函数可能永远运行。变体 it.ensureTermination.toListRev 总会在有限步后终止。