22.2. 迭代器定义🔗

迭代器可以是单子式或纯的，也可以是有限、能产或潜在无限的。 单子式迭代器使用某个单子中的副作用来发出各个值，因此必须在该单子中使用；而纯迭代器不需要副作用。例如，迭代目录中的所有文件需要 IO 单子。纯迭代器的类型为 Iter，单子式迭代器则由 IterM 表示。

结构体

Std.Iter.{w} {α : Type w} (β : Type w) : Type w
Std.Iter.{w} {α : Type w} (β : Type w) :
  Type w

一种依次发出 β 类型值的迭代器。它可以是有限的，也可以是无限的。

迭代器框架的更全面概览见根模块 Std.Data.Iterators。

如何迭代常见数据结构见 Std.Data.Iterators.Producers。按照约定，与对象关联的单子式迭代器可通过点记法取得。例如，List.iterM IO 会在单子 IO 中创建一个遍历列表的迭代器。

迭代器的使用方式见 Init.Data.Iterators.Consumers。例如，it.toList 会把迭代器 it 转换为列表；若有该迭代器有限的证明，it.ensureTermination.toList 可保证此操作终止。也始终可以用 it.step 手动迭代，并以终止度量 it.finitelyManySteps 和 it.finitelyManySkips 证明终止。

在单子中运行的迭代器见 IterM。

在内部，Iter β 包装一个包含状态信息的 α 类型元素。类型 α 通过类型类机制决定迭代器的实现；实际实现迭代器的类型类是 Iterator α m β。

使用组合子时，α 可能变得非常复杂。它是 α 的隐式参数，因此漂亮打印器默认不会打印这个庞大类型。若声明返回迭代器，以下写法不可行：

def x : Iter Nat := [1, 2, 3].iter

应当完全省略声明的类型：

def x := [1, 2, 3].iter

-- 若要确保 `x` 是发出 `Nat` 的迭代器
def x := ([1, 2, 3].iter : Iter Nat)

构造子

Std.Iter.mk.{w}

字段

internalState : α

迭代器的内部实现细节。

结构体

Std.IterM.{w, w'} {α : Type w} (m : Type w → Type w') (β : Type w) :
  Type w
Std.IterM.{w, w'} {α : Type w}
  (m : Type w → Type w') (β : Type w) :
  Type w

一种在单子 m 中依次发出 β 类型值的迭代器。它可以是有限的，也可以是无限的。

迭代器框架的更全面概览见根模块 Std.Data.Iterators。

若不需要单子式效应（m = Id），可使用接口更方便的 Iter。

在内部，IterM m β 包装一个包含状态信息的 α 类型元素。类型 α 通过类型类机制决定迭代器的实现；实际实现迭代器的类型类是 Iterator α m β。

使用组合子时，α 可能变得非常复杂。它是 α 的隐式参数，因此漂亮打印器默认不会打印这个庞大类型。若声明返回迭代器，以下写法不可行：

def x : IterM IO Nat := [1, 2, 3].iterM IO

应当完全省略声明的类型：

def x := [1, 2, 3].iterM IO

-- 若要确保 `x` 是在 `IO` 中发出 `Nat` 的迭代器
def x := ([1, 2, 3].iterM IO : IterM IO Nat)

构造子

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

将迭代器状态包装为 IterM 对象。

字段

internalState : α

迭代器的内部实现细节。

类型 Iter 和 IterM 只是内部状态的包装。该内部状态类型是迭代器类型的隐式参数。对于 List.iter 所产生的这类基本生产者迭代器，该类型相当简单；但由组合子产生的迭代器会使用可能变得很庞大的多态状态类型。由于 Lean 会先精译函数指定的返回类型，再精译其函数体，因此可能无法自动确定函数所返回迭代器类型的内部状态类型。此时可以省略签名中的返回类型，改在定义体上添加类型标注，从而让定义体中调用的具体迭代器组合子参与确定状态类型。

迭代器状态类型

可以显式写出列表与数组迭代器的内部状态类型：

def reds := ["red", "crimson"]

example : @Iter (ListIterator String) String := reds.iter

example : @Iter (ArrayIterator String) String := reds.toArray.iter

但使用 Iter.map 组合子时，其内部状态类型相当复杂：

example :
    @Iter
      (Map (ListIterator String) Id Id @id fun x : String =>
        pure x.length)
      Nat :=
  reds.iter.map String.length

省略状态类型会导致错误：

example : don't know how to synthesize implicit argument `α`
  @Iter ?m.1 Nat
context:
⊢ Type

Note: Because this declaration's type has been explicitly provided, all parameter types and holes (e.g., `_`) in its header are resolved before its body is processed; information from the declaration body cannot be used to infer what these values should beIter Nat := reds.iter.map String.length

don't know how to synthesize implicit argument `α`
  @Iter ?m.1 Nat
context:
⊢ Type

Note: Because this declaration's type has been explicitly provided, all parameter types and holes (e.g., `_`) in its header are resolved before its body is processed; information from the declaration body cannot be used to infer what these values should be

与其手写状态类型，不如省略返回类型，改在项的外部提供标注：

example := (reds.iter.map String.length : Iter Nat)

example :=
  show Iter Nat from
  reds.iter.map String.length

在线查看 ↪

实际的迭代过程是在收到请求时产生一系列迭代步骤。每一步都会返回具有新内部状态的更新后迭代器，同时还会返回以下三者之一：数据值（IterStep.yield）、提示调用方应再次请求数据值的标志（IterStep.skip），或迭代已经结束的标志（IterStep.done）。若不能使用 skip，就会很难处理 Iter.filter 这类不会为底层迭代器发出的每个值都产出结果的迭代器组合子。借助 skip，filter 的实现无需为了成为良定义函数而考虑底层迭代器是否有限；关于其有限性的推理可以在单独的证明中完成。此外，否则 filter 还需要一个内层循环，而编译器很难将其内联。

归纳类型

Std.IterStep.{u_1, u_2} (α : Sort u_1) (β : Sort u_2) :
  Sort (max (max 1 u_1) u_2)
Std.IterStep.{u_1, u_2} (α : Sort u_1)
  (β : Sort u_2) :
  Sort (max (max 1 u_1) u_2)

IterStep α β 表示迭代器（Iter β 或 IterM m β）执行的一步。

构造子

Std.IterStep.yield.{u_1, u_2} {α : Sort u_1} {β : Sort u_2}
  (it : α) (out : β) : IterStep α β

IterStep.yield it out 表示迭代器发出 out，并以 it 作为后继迭代器。

Std.IterStep.skip.{u_1, u_2} {α : Sort u_1} {β : Sort u_2}
  (it : α) : IterStep α β

IterStep.skip it 表示迭代器本次迭代不发出任何值，并以 it' 作为后继迭代器。

允许 skip 步骤是为了让迭代器循环能生成高效代码。

Std.IterStep.done.{u_1, u_2} {α : Sort u_1} {β : Sort u_2} :
  IterStep α β

IterStep.done 表示迭代器已经结束，不会再发出值，也不会再产生单子式效应；此时不提供后继迭代器。

Iter 和 IterM 所执行的步骤分别由类型 Iter.Step 和 IterM.Step 表示。这两种步骤类型都是 IterStep 的包装，其中包含用于跟踪终止行为的额外证明。

定义

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

Iter.step 返回的步骤对象类型，其中包含一个 IterStep，以及它是给定迭代器之合理步骤的证明。

定义

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

IterM.step 返回的步骤对象类型，其中包含一个 IterStep，以及它是给定迭代器之合理步骤的证明。

迭代器通过 Iterator.step 产生步骤；它是 Iterator 类型类的方法。 Iterator 同时用于纯迭代器和单子式迭代器；纯迭代器可以对单子的选择完全多态，因此调用方可以用 Id 将其实例化。

类型类

Std.Iterator.{w, w'} (α : Type w) (m : Type w → Type w')
  (β : outParam (Type w)) : Type (max w w')
Std.Iterator.{w, w'} (α : Type w)
  (m : Type w → Type w')
  (β : outParam (Type w)) :
  Type (max w w')

Iter (α := α) β 或 IterM (α := α) m β 中迭代器的步进函数。

为了在使用 step 函数迭代时支持内蕴的终止性证明，步骤对象还携带一个证明，表明它是给定当前迭代器的“合理”步骤。

实例构造子

Std.Iterator.mk.{w, w'}

方法

IsPlausibleStep : IterM m β → IterStep (IterM m β) β → Prop

支配给定迭代器所允许步骤的关系。

“合理”步骤是对给定状态有意义的步骤；合理性可保证诸如后继迭代器仍来自同一集合、跳过所得迭代器会返回相同的下一个值，或下一个产出项确为原集合中的下一项等性质。

step : (it : IterM m β) → m (Std.Shrink (PlausibleIterStep (Iterator.IsPlausibleStep it)))

执行一个迭代步骤。

22.2.1. 合理性🔗

除了步骤函数，Iterator 的实例还包含关系 Iterator.IsPlausibleStep。该关系之所以存在，是因为大多数迭代器既会维持其内部状态上的不变量，也会以可预测的方式产出值。例如，数组迭代器会同时跟踪一个数组以及指向其中的当前索引。推进数组迭代器会得到仍遍历同一底层数组的迭代器；当索引足够小时它会产出一个值，否则便结束。从某个迭代器状态出发的合理步骤，是指通过该迭代器对 IsPlausibleStep 的实现而与该状态相关的步骤。在逻辑层面跟踪合理性，使得推理单子式迭代器的终止行为成为可能。

Iter.Step 与 IterM.Step 都以 PlausibleIterStep 定义；因此，这两种类型都可以对其命名空间使用前导点记法。可以使用三个匹配模式函数 PlausibleIterStep.yield、PlausibleIterStep.skip 和 PlausibleIterStep.done 分析 Iter.Step 或 IterM.Step。这些函数把底层 IterStep 中的信息与其外围证明对象配对。

定义

Std.PlausibleIterStep.{u, w} {α : Type u} {β : Type w}
  (IsPlausibleStep : IterStep α β → Prop) : Type (max 0 u w)
Std.PlausibleIterStep.{u, w} {α : Type u}
  {β : Type w}
  (IsPlausibleStep :
    IterStep α β → Prop) :
  Type (max 0 u w)

IterStep 的一种变体，将步骤与该步骤“合理”的证明打包在一起。之后会选择合理性谓词来断言某个状态是另一状态的合理后继。将此证明与步骤打包对终止性证明很重要。

合理性谓词的具体选择见 IterM.Step 和 Iter.Step。

定义

Std.PlausibleIterStep.yield.{u, w} {α : Type u} {β : Type w}
  {IsPlausibleStep : IterStep α β → Prop} (it' : α) (out : β)
  (h : IsPlausibleStep (IterStep.yield it' out)) :
  PlausibleIterStep IsPlausibleStep
Std.PlausibleIterStep.yield.{u, w}
  {α : Type u} {β : Type w}
  {IsPlausibleStep : IterStep α β → Prop}
  (it' : α) (out : β)
  (h :
    IsPlausibleStep
      (IterStep.yield it' out)) :
  PlausibleIterStep IsPlausibleStep

yield 情形的模式。另见 IterStep.yield。

定义

Std.PlausibleIterStep.skip.{u, w} {α : Type u} {β : Type w}
  {IsPlausibleStep : IterStep α β → Prop} (it' : α)
  (h : IsPlausibleStep (IterStep.skip it')) :
  PlausibleIterStep IsPlausibleStep
Std.PlausibleIterStep.skip.{u, w}
  {α : Type u} {β : Type w}
  {IsPlausibleStep : IterStep α β → Prop}
  (it' : α)
  (h :
    IsPlausibleStep (IterStep.skip it')) :
  PlausibleIterStep IsPlausibleStep

skip 情形的模式。另见 IterStep.skip。

定义

Std.PlausibleIterStep.done.{u, w} {α : Type u} {β : Type w}
  {IsPlausibleStep : IterStep α β → Prop}
  (h : IsPlausibleStep IterStep.done) :
  PlausibleIterStep IsPlausibleStep
Std.PlausibleIterStep.done.{u, w}
  {α : Type u} {β : Type w}
  {IsPlausibleStep : IterStep α β → Prop}
  (h : IsPlausibleStep IterStep.done) :
  PlausibleIterStep IsPlausibleStep

done 情形的模式。另见 IterStep.done。

22.2.2. 有限且能产的迭代器🔗

并非所有迭代器都保证返回有限个结果；遍历所有自然数完全合理。同样，并非所有迭代器都保证返回一个结果或终止；迭代器可以用任意程序定义。因此，Lean 将迭代器分为三类终止性类别：

有限迭代器保证在有限步后结束迭代。这些迭代器具有 Finite 实例。
能产迭代器保证在有限步内产出一个值或终止，但它们可能产出无限多个值。这些迭代器具有 Productive 实例。
其余终止行为未知的迭代器。这些迭代器不具有上述任何一种实例。

所有有限迭代器必然都是能产的。

类型类

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

Finite α m 断言 IterM (α := α) m 会在有限步后终止。技术上说，这意味着合理后继关系是良基的。有了此类型类，以迭代器 it 进行良基递归时，可以用 it.finitelyManySteps 作为终止度量。

实例构造子

Std.Iterators.Finite.mk.{w, w'}

方法

wf : WellFounded IterM.IsPlausibleSuccessorOf

合理后继关系是良基的。

类型类

Std.Iterators.Productive.{u_1, u_2} (α : Type u_1)
  (m : Type u_1 → Type u_2) {β : Type u_1} [Iterator α m β] : Prop
Std.Iterators.Productive.{u_1, u_2}
  (α : Type u_1) (m : Type u_1 → Type u_2)
  {β : Type u_1} [Iterator α m β] : Prop

Productive α m 断言 IterM (α := α) m 会在有限次跳过后终止或发出一个值。技术上说，这意味着跳过期间的合理后继关系是良基的。有了此类型类，以迭代器 it 进行良基递归时，可以用 it.finitelyManySkips 作为终止度量。

实例构造子

Std.Iterators.Productive.mk.{u_1, u_2}

方法

wf : WellFounded IterM.IsPlausibleSkipSuccessorOf

跳过期间的合理后继关系是良基的。

Lean 标准库提供了许多遍历迭代器的函数。这些消费者函数通常不会对底层迭代器作任何假设。尤其是，对某些迭代器而言，这类函数可能永远运行下去。

有时，确保函数确实终止至关重要。在这些情况下，组合子 Iter.ensureTermination 会得到一种迭代器，它提供保证终止的消费者变体。这些变体通常要求证明所涉及的迭代器是有限的。

定义

Std.Iter.ensureTermination.{w} {α β : Type w} (it : Iter β) :
  Iter.Total β
Std.Iter.ensureTermination.{w}
  {α β : Type w} (it : Iter β) :
  Iter.Total β

对于迭代器 it，it.ensureTermination 提供一定会终止的消费者变体。

定义

Std.IterM.ensureTermination.{w, w'} {α β : Type w}
  {m : Type w → Type w'} (it : IterM m β) : IterM.Total m β
Std.IterM.ensureTermination.{w, w'}
  {α β : Type w} {m : Type w → Type w'}
  (it : IterM m β) : IterM.Total m β

对于迭代器 it，it.ensureTermination 提供一定会终止的消费者变体。

迭代 Nat

要编写依次产出每个自然数的迭代器，第一步是实现其内部状态。该迭代器只需记住下一个自然数：

structure Nats where
  next : Nat

该迭代器只会产出下一个自然数。因此，它的步骤函数绝不会返回 skip 或 done。每当它产出一个值时，该值就是内部状态的 next 字段，而后继迭代器的 next 字段则会增加一。 grind 策略足以证明该步骤确实合理：

instance [Pure m] : Iterator Nats m Nat where
  IsPlausibleStep it
    | .yield it' n =>
      n = it.internalState.next ∧
      it'.internalState.next = n + 1
    | _ => False
  step it :=
    let n := it.internalState.next
    pure <| .deflate <|
      .yield { it with internalState.next := n + 1 } n (bym:Type → Type ?u.3inst✝:Pure mit:IterM m Natn:Nat := it.internalState.next⊢ match
  IterStep.yield
    {
      internalState :=
        let __src := it.internalState;
        { next := n + 1 } }
    n with
| IterStep.yield it' n => n = it.internalState.next ∧ it'.internalState.next = n + 1
| x => False grindAll goals completed! 🐙)

每当定义迭代器时，都应提供 IteratorLoop 实例。 Iter.toList 或 for 循环等大多数迭代器消费者都需要它。可以如下使用其默认实现：

instance [Pure m] [Monad n] : IteratorLoop Nats m n :=
  .defaultImplementation

此 step 函数是能产的，因为它绝不返回 skip。因此，要证明每条 skip 链长度有限，可以利用这一事实：当 it 是 Nats 迭代器时，Iterator.IsPlausibleStep it (.skip it') = False：

instance [Pure m] : Productive Nats m where
  wf := .intro <| fun _ => .intro _ nofun

因为 Nat 有无限多个，所以该迭代器不是有限的。

可以使用此函数创建 Nats 迭代器：

def Nats.iter : Iter (α := Nats) Nat :=
  IterM.mk { next := 0 } |>.toIter

运行以下函数可以打印所有自然数：

def f : IO Unit := do
  for x in Nats.iter do
    IO.println s!"{x}"

该函数永不终止，它会按递增顺序逐个打印所有自然数。

该迭代器与 Iter.zip 等组合子配合使用时最为有用：

0: cat
1: dog
2: pachycephalosaurus
#eval show IO Unit from do
  let xs : List String := ["cat", "dog", "pachycephalosaurus"]
  for (x, y) in Nats.iter.zip xs.iter do
    IO.println s!"{x}: {y}"

0: cat
1: dog
2: pachycephalosaurus

与前例不同，该循环会终止，因为 xs.iter 是有限迭代器。可以通过提供 Finite 实例来确保循环确实终止：

Zip Nats Id (ListIterator String) String : Type#check type_of% (Nats.iter.zip ["cat", "dog"].iter).internalState

Zip.instFinite₂#synth Finite (Zip Nats Id (ListIterator String) String) Id

Zip Nats Id (ListIterator String) String : Type

Zip.instFinite₂

相比之下，Nats.iter 会产出无限多个值，因此没有 Finite 实例：

failed to synthesize
  Finite Nats Id

Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.#synth Finite Nats Id

failed to synthesize
  Finite Nats Id

Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.

因为 Nat 有无限多个，使用 Iter.ensureTermination 会导致错误：

#eval show IO Unit from do
  failed to synthesize instance of type class
  ForIn IO (Iter.Total Nat) ?α

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.for x in Nats.iter.ensureTermination do
    IO.println s!"{x}"

failed to synthesize instance of type class
  ForIn IO (Iter.Total Nat) ?α

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

在线查看 ↪

迭代三元组

类型 Triple 包含三个相同类型的值：

structure Triple α where
  fst : α
  snd : α
  thd : α

遍历 Triple 的迭代器，其内部状态可以由一个三元组和当前位置配对组成。该位置可以是其中一个字段，也可以表示迭代已结束。

inductive TriplePos where
  | fst | snd | thd | done

可以使用位置查找元素：

def Triple.get? (xs : Triple α) (pos : TriplePos) : Option α :=
  match pos with
  | .fst => some xs.fst
  | .snd => some xs.snd
  | .thd => some xs.thd
  | _ => none

每个字段位置都有一个后继位置：

@[grind, grind cases]
inductive TriplePos.Succ : TriplePos → TriplePos → Prop where
  | fst : Succ .fst .snd
  | snd : Succ .snd .thd
  | thd : Succ .thd .done

迭代器本身将三元组与下一个元素的位置配对：

structure TripleIterator α where
  triple : Triple α
  pos : TriplePos

迭代从 fst 开始：

def Triple.iter (xs : Triple α) : Iter (α := TripleIterator α) α :=
  IterM.mk {triple := xs, pos := .fst : TripleIterator α} |>.toIter

有两种合理步骤：若迭代器的位置存在后继，则下一个迭代器仍指向同一三元组，但位置变为后继位置；若不存在后继，则迭代完成。

@[grind]
inductive TripleIterator.IsPlausibleStep :
    @IterM (TripleIterator α) m α →
    IterStep (@IterM (TripleIterator α) m α) α →
    Prop where
  | yield :
    it.internalState.triple = it'.internalState.triple →
    it.internalState.pos.Succ it'.internalState.pos →
    it.internalState.triple.get? it.internalState.pos = some out →
    IsPlausibleStep it (.yield it' out)
  | done :
    it.internalState.pos = .done →
    IsPlausibleStep it .done

对应的步骤函数会产出该关系所描述的迭代器和值：

instance [Pure m] : Iterator (TripleIterator α) m α where
  IsPlausibleStep := TripleIterator.IsPlausibleStep
  step
    | ⟨xs, pos⟩ =>
      pure <| .deflate <|
      match pos with
      | .fst => .yield ⟨xs, .snd⟩ xs.fst ?_
      | .snd => .yield ⟨xs, .thd⟩ xs.snd ?_
      | .thd => .yield ⟨xs, .done⟩ xs.thd ?_
      | .done => .done <| ?_
where finally
  all_goals grind [Triple.get?]All goals completed! 🐙

现在可以将该迭代器转换为数组：

def abc : Triple Char := ⟨'a', 'b', 'c'⟩

#['a', 'b', 'c']#eval abc.iter.toArray

#['a', 'b', 'c']

一般而言，Iter.toArray 可能永远运行。可以通过构造 Finite (Triple Char) Id 实例来证明 abc 是有限的，并证明上例会在有限步后终止。最简单的做法是从 TriplePos.done 开始，反向推至 TriplePos.fst，依次证明每个位置都只有有限长的后继链：

@[grind! .]
theorem acc_done [Pure m] :
    Acc (IterM.IsPlausibleSuccessorOf (m := m))
      ⟨{ triple, pos := .done : TripleIterator α}⟩ :=
  Acc.intro _ fun
    | _, ⟨_, ⟨_, h⟩⟩ =>m:Type u_1 → Type u_2α:Type u_1triple:Triple αinst✝:Pure mx✝:IterM m αw✝:IterStep (IterM m α) αleft✝:w✝.successor = some x✝h:{ internalState := { triple := triple, pos := TriplePos.done } }.IsPlausibleStep w✝⊢ Acc IterM.IsPlausibleSuccessorOf x✝ bym:Type u_1 → Type u_2α:Type u_1triple:Triple αinst✝:Pure mx✝:IterM m αw✝:IterStep (IterM m α) αleft✝:w✝.successor = some x✝h:{ internalState := { triple := triple, pos := TriplePos.done } }.IsPlausibleStep w✝⊢ Acc IterM.IsPlausibleSuccessorOf x✝
      cases hyieldm:Type u_1 → Type u_2α:Type u_1triple:Triple αinst✝:Pure mx✝:IterM m αout✝:αit'✝:IterM m αa✝²:{ internalState := { triple := triple, pos := TriplePos.done } }.internalState.triple = it'✝.internalState.triplea✝¹:{ internalState := { triple := triple, pos := TriplePos.done } }.internalState.pos.Succ it'✝.internalState.posa✝:{ internalState := { triple := triple, pos := TriplePos.done } }.internalState.triple.get?
    { internalState := { triple := triple, pos := TriplePos.done } }.internalState.pos =
  some out✝left✝:(IterStep.yield it'✝ out✝).successor = some x✝⊢ Acc IterM.IsPlausibleSuccessorOf x✝donem:Type u_1 → Type u_2α:Type u_1triple:Triple αinst✝:Pure mx✝:IterM m αa✝:{ internalState := { triple := triple, pos := TriplePos.done } }.internalState.pos = TriplePos.doneleft✝:IterStep.done.successor = some x✝⊢ Acc IterM.IsPlausibleSuccessorOf x✝ <;>yieldm:Type u_1 → Type u_2α:Type u_1triple:Triple αinst✝:Pure mx✝:IterM m αout✝:αit'✝:IterM m αa✝²:{ internalState := { triple := triple, pos := TriplePos.done } }.internalState.triple = it'✝.internalState.triplea✝¹:{ internalState := { triple := triple, pos := TriplePos.done } }.internalState.pos.Succ it'✝.internalState.posa✝:{ internalState := { triple := triple, pos := TriplePos.done } }.internalState.triple.get?
    { internalState := { triple := triple, pos := TriplePos.done } }.internalState.pos =
  some out✝left✝:(IterStep.yield it'✝ out✝).successor = some x✝⊢ Acc IterM.IsPlausibleSuccessorOf x✝donem:Type u_1 → Type u_2α:Type u_1triple:Triple αinst✝:Pure mx✝:IterM m αa✝:{ internalState := { triple := triple, pos := TriplePos.done } }.internalState.pos = TriplePos.doneleft✝:IterStep.done.successor = some x✝⊢ Acc IterM.IsPlausibleSuccessorOf x✝ grind [IterStep.successor_done]All goals completed! 🐙

@[grind! .]
theorem acc_thd [Pure m] :
    Acc (IterM.IsPlausibleSuccessorOf (m := m))
      ⟨{ triple, pos := .thd : TripleIterator α}⟩ :=
  Acc.intro _ fun
    | ⟨{ triple, pos }⟩, ⟨h, h', h''⟩ =>m:Type u_1 → Type u_2α:Type u_1triple✝:Triple αinst✝:Pure mtriple:Triple αpos:TriplePosh:IterStep (IterM m α) αh':h.successor = some { internalState := { triple := triple, pos := pos } }h'':{ internalState := { triple := triple✝, pos := TriplePos.thd } }.IsPlausibleStep h⊢ Acc IterM.IsPlausibleSuccessorOf { internalState := { triple := triple, pos := pos } } bym:Type u_1 → Type u_2α:Type u_1triple✝:Triple αinst✝:Pure mtriple:Triple αpos:TriplePosh:IterStep (IterM m α) αh':h.successor = some { internalState := { triple := triple, pos := pos } }h'':{ internalState := { triple := triple✝, pos := TriplePos.thd } }.IsPlausibleStep h⊢ Acc IterM.IsPlausibleSuccessorOf { internalState := { triple := triple, pos := pos } }
      cases h''yieldm:Type u_1 → Type u_2α:Type u_1triple✝:Triple αinst✝:Pure mtriple:Triple αpos:TriplePosout✝:αit'✝:IterM m αa✝²:{ internalState := { triple := triple✝, pos := TriplePos.thd } }.internalState.triple = it'✝.internalState.triplea✝¹:{ internalState := { triple := triple✝, pos := TriplePos.thd } }.internalState.pos.Succ it'✝.internalState.posa✝:{ internalState := { triple := triple✝, pos := TriplePos.thd } }.internalState.triple.get?
    { internalState := { triple := triple✝, pos := TriplePos.thd } }.internalState.pos =
  some out✝h':(IterStep.yield it'✝ out✝).successor = some { internalState := { triple := triple, pos := pos } }⊢ Acc IterM.IsPlausibleSuccessorOf { internalState := { triple := triple, pos := pos } }donem:Type u_1 → Type u_2α:Type u_1triple✝:Triple αinst✝:Pure mtriple:Triple αpos:TriplePosa✝:{ internalState := { triple := triple✝, pos := TriplePos.thd } }.internalState.pos = TriplePos.doneh':IterStep.done.successor = some { internalState := { triple := triple, pos := pos } }⊢ Acc IterM.IsPlausibleSuccessorOf { internalState := { triple := triple, pos := pos } } <;>yieldm:Type u_1 → Type u_2α:Type u_1triple✝:Triple αinst✝:Pure mtriple:Triple αpos:TriplePosout✝:αit'✝:IterM m αa✝²:{ internalState := { triple := triple✝, pos := TriplePos.thd } }.internalState.triple = it'✝.internalState.triplea✝¹:{ internalState := { triple := triple✝, pos := TriplePos.thd } }.internalState.pos.Succ it'✝.internalState.posa✝:{ internalState := { triple := triple✝, pos := TriplePos.thd } }.internalState.triple.get?
    { internalState := { triple := triple✝, pos := TriplePos.thd } }.internalState.pos =
  some out✝h':(IterStep.yield it'✝ out✝).successor = some { internalState := { triple := triple, pos := pos } }⊢ Acc IterM.IsPlausibleSuccessorOf { internalState := { triple := triple, pos := pos } }donem:Type u_1 → Type u_2α:Type u_1triple✝:Triple αinst✝:Pure mtriple:Triple αpos:TriplePosa✝:{ internalState := { triple := triple✝, pos := TriplePos.thd } }.internalState.pos = TriplePos.doneh':IterStep.done.successor = some { internalState := { triple := triple, pos := pos } }⊢ Acc IterM.IsPlausibleSuccessorOf { internalState := { triple := triple, pos := pos } } grind [IterStep.successor_yield]All goals completed! 🐙

@[grind! .]
theorem acc_snd [Pure m] :
    Acc (IterM.IsPlausibleSuccessorOf (m := m))
      ⟨{ triple, pos := .snd : TripleIterator α}⟩ :=
  Acc.intro _ fun
    | ⟨{ triple, pos }⟩, ⟨h, h', h''⟩ =>m:Type u_1 → Type u_2α:Type u_1triple✝:Triple αinst✝:Pure mtriple:Triple αpos:TriplePosh:IterStep (IterM m α) αh':h.successor = some { internalState := { triple := triple, pos := pos } }h'':{ internalState := { triple := triple✝, pos := TriplePos.snd } }.IsPlausibleStep h⊢ Acc IterM.IsPlausibleSuccessorOf { internalState := { triple := triple, pos := pos } } bym:Type u_1 → Type u_2α:Type u_1triple✝:Triple αinst✝:Pure mtriple:Triple αpos:TriplePosh:IterStep (IterM m α) αh':h.successor = some { internalState := { triple := triple, pos := pos } }h'':{ internalState := { triple := triple✝, pos := TriplePos.snd } }.IsPlausibleStep h⊢ Acc IterM.IsPlausibleSuccessorOf { internalState := { triple := triple, pos := pos } }
      cases h''yieldm:Type u_1 → Type u_2α:Type u_1triple✝:Triple αinst✝:Pure mtriple:Triple αpos:TriplePosout✝:αit'✝:IterM m αa✝²:{ internalState := { triple := triple✝, pos := TriplePos.snd } }.internalState.triple = it'✝.internalState.triplea✝¹:{ internalState := { triple := triple✝, pos := TriplePos.snd } }.internalState.pos.Succ it'✝.internalState.posa✝:{ internalState := { triple := triple✝, pos := TriplePos.snd } }.internalState.triple.get?
    { internalState := { triple := triple✝, pos := TriplePos.snd } }.internalState.pos =
  some out✝h':(IterStep.yield it'✝ out✝).successor = some { internalState := { triple := triple, pos := pos } }⊢ Acc IterM.IsPlausibleSuccessorOf { internalState := { triple := triple, pos := pos } }donem:Type u_1 → Type u_2α:Type u_1triple✝:Triple αinst✝:Pure mtriple:Triple αpos:TriplePosa✝:{ internalState := { triple := triple✝, pos := TriplePos.snd } }.internalState.pos = TriplePos.doneh':IterStep.done.successor = some { internalState := { triple := triple, pos := pos } }⊢ Acc IterM.IsPlausibleSuccessorOf { internalState := { triple := triple, pos := pos } } <;>yieldm:Type u_1 → Type u_2α:Type u_1triple✝:Triple αinst✝:Pure mtriple:Triple αpos:TriplePosout✝:αit'✝:IterM m αa✝²:{ internalState := { triple := triple✝, pos := TriplePos.snd } }.internalState.triple = it'✝.internalState.triplea✝¹:{ internalState := { triple := triple✝, pos := TriplePos.snd } }.internalState.pos.Succ it'✝.internalState.posa✝:{ internalState := { triple := triple✝, pos := TriplePos.snd } }.internalState.triple.get?
    { internalState := { triple := triple✝, pos := TriplePos.snd } }.internalState.pos =
  some out✝h':(IterStep.yield it'✝ out✝).successor = some { internalState := { triple := triple, pos := pos } }⊢ Acc IterM.IsPlausibleSuccessorOf { internalState := { triple := triple, pos := pos } }donem:Type u_1 → Type u_2α:Type u_1triple✝:Triple αinst✝:Pure mtriple:Triple αpos:TriplePosa✝:{ internalState := { triple := triple✝, pos := TriplePos.snd } }.internalState.pos = TriplePos.doneh':IterStep.done.successor = some { internalState := { triple := triple, pos := pos } }⊢ Acc IterM.IsPlausibleSuccessorOf { internalState := { triple := triple, pos := pos } } grind [IterStep.successor_yield]All goals completed! 🐙

@[grind! .]
theorem acc_fst [Pure m] :
    Acc (IterM.IsPlausibleSuccessorOf (m := m))
      ⟨{ triple, pos := .fst : TripleIterator α}⟩ :=
  Acc.intro _ fun
    | ⟨{ triple, pos }⟩, ⟨h, h', h''⟩ =>m:Type u_1 → Type u_2α:Type u_1triple✝:Triple αinst✝:Pure mtriple:Triple αpos:TriplePosh:IterStep (IterM m α) αh':h.successor = some { internalState := { triple := triple, pos := pos } }h'':{ internalState := { triple := triple✝, pos := TriplePos.fst } }.IsPlausibleStep h⊢ Acc IterM.IsPlausibleSuccessorOf { internalState := { triple := triple, pos := pos } } bym:Type u_1 → Type u_2α:Type u_1triple✝:Triple αinst✝:Pure mtriple:Triple αpos:TriplePosh:IterStep (IterM m α) αh':h.successor = some { internalState := { triple := triple, pos := pos } }h'':{ internalState := { triple := triple✝, pos := TriplePos.fst } }.IsPlausibleStep h⊢ Acc IterM.IsPlausibleSuccessorOf { internalState := { triple := triple, pos := pos } }
      cases h''yieldm:Type u_1 → Type u_2α:Type u_1triple✝:Triple αinst✝:Pure mtriple:Triple αpos:TriplePosout✝:αit'✝:IterM m αa✝²:{ internalState := { triple := triple✝, pos := TriplePos.fst } }.internalState.triple = it'✝.internalState.triplea✝¹:{ internalState := { triple := triple✝, pos := TriplePos.fst } }.internalState.pos.Succ it'✝.internalState.posa✝:{ internalState := { triple := triple✝, pos := TriplePos.fst } }.internalState.triple.get?
    { internalState := { triple := triple✝, pos := TriplePos.fst } }.internalState.pos =
  some out✝h':(IterStep.yield it'✝ out✝).successor = some { internalState := { triple := triple, pos := pos } }⊢ Acc IterM.IsPlausibleSuccessorOf { internalState := { triple := triple, pos := pos } }donem:Type u_1 → Type u_2α:Type u_1triple✝:Triple αinst✝:Pure mtriple:Triple αpos:TriplePosa✝:{ internalState := { triple := triple✝, pos := TriplePos.fst } }.internalState.pos = TriplePos.doneh':IterStep.done.successor = some { internalState := { triple := triple, pos := pos } }⊢ Acc IterM.IsPlausibleSuccessorOf { internalState := { triple := triple, pos := pos } } <;>yieldm:Type u_1 → Type u_2α:Type u_1triple✝:Triple αinst✝:Pure mtriple:Triple αpos:TriplePosout✝:αit'✝:IterM m αa✝²:{ internalState := { triple := triple✝, pos := TriplePos.fst } }.internalState.triple = it'✝.internalState.triplea✝¹:{ internalState := { triple := triple✝, pos := TriplePos.fst } }.internalState.pos.Succ it'✝.internalState.posa✝:{ internalState := { triple := triple✝, pos := TriplePos.fst } }.internalState.triple.get?
    { internalState := { triple := triple✝, pos := TriplePos.fst } }.internalState.pos =
  some out✝h':(IterStep.yield it'✝ out✝).successor = some { internalState := { triple := triple, pos := pos } }⊢ Acc IterM.IsPlausibleSuccessorOf { internalState := { triple := triple, pos := pos } }donem:Type u_1 → Type u_2α:Type u_1triple✝:Triple αinst✝:Pure mtriple:Triple αpos:TriplePosa✝:{ internalState := { triple := triple✝, pos := TriplePos.fst } }.internalState.pos = TriplePos.doneh':IterStep.done.successor = some { internalState := { triple := triple, pos := pos } }⊢ Acc IterM.IsPlausibleSuccessorOf { internalState := { triple := triple, pos := pos } } grind [IterStep.successor_yield]All goals completed! 🐙

instance [Pure m] : Finite (TripleIterator α) m where
  wf := .intro <| fun
    | { internalState := { triple, pos } } =>m:Type u_1 → Type u_2α:Type u_1inst✝:Pure mtriple:Triple αpos:TriplePos⊢ Acc IterM.IsPlausibleSuccessorOf { internalState := { triple := triple, pos := pos } } bym:Type u_1 → Type u_2α:Type u_1inst✝:Pure mtriple:Triple αpos:TriplePos⊢ Acc IterM.IsPlausibleSuccessorOf { internalState := { triple := triple, pos := pos } }
      cases posfstm:Type u_1 → Type u_2α:Type u_1inst✝:Pure mtriple:Triple α⊢ Acc IterM.IsPlausibleSuccessorOf { internalState := { triple := triple, pos := TriplePos.fst } }sndm:Type u_1 → Type u_2α:Type u_1inst✝:Pure mtriple:Triple α⊢ Acc IterM.IsPlausibleSuccessorOf { internalState := { triple := triple, pos := TriplePos.snd } }thdm:Type u_1 → Type u_2α:Type u_1inst✝:Pure mtriple:Triple α⊢ Acc IterM.IsPlausibleSuccessorOf { internalState := { triple := triple, pos := TriplePos.thd } }donem:Type u_1 → Type u_2α:Type u_1inst✝:Pure mtriple:Triple α⊢ Acc IterM.IsPlausibleSuccessorOf { internalState := { triple := triple, pos := TriplePos.done } } <;>fstm:Type u_1 → Type u_2α:Type u_1inst✝:Pure mtriple:Triple α⊢ Acc IterM.IsPlausibleSuccessorOf { internalState := { triple := triple, pos := TriplePos.fst } }sndm:Type u_1 → Type u_2α:Type u_1inst✝:Pure mtriple:Triple α⊢ Acc IterM.IsPlausibleSuccessorOf { internalState := { triple := triple, pos := TriplePos.snd } }thdm:Type u_1 → Type u_2α:Type u_1inst✝:Pure mtriple:Triple α⊢ Acc IterM.IsPlausibleSuccessorOf { internalState := { triple := triple, pos := TriplePos.thd } }donem:Type u_1 → Type u_2α:Type u_1inst✝:Pure mtriple:Triple α⊢ Acc IterM.IsPlausibleSuccessorOf { internalState := { triple := triple, pos := TriplePos.done } } grindAll goals completed! 🐙

要使该迭代器可用于 Lean.Parser.Term.doFor : doElemfor 循环，需要一个 IteratorLoop 实例：

instance [Monad m] [Monad n] :
    IteratorLoop (TripleIterator α) m n :=
  .defaultImplementation

a
b
c
#eval show IO Unit from do
  for x in abc.iter do
    IO.println x

a
b
c

在线查看 ↪

迭代器与效果

遍历文件内容的一种方式，是在每一步从 Stream 读取指定数量的字节。到达文件末尾时，迭代器可以让引用计数降为零，从而关闭文件：

structure FileIterator where
  stream? : Option IO.FS.Stream
  count : USize := 8192

可以打开文件并将其句柄转换为流，以创建迭代器：

def iterFile
    (path : System.FilePath)
    (count : USize := 8192) :
    IO (IterM (α := FileIterator) IO ByteArray) := do
  let h ← IO.FS.Handle.mk path .read
  let stream? := some (IO.FS.Stream.ofHandle h)
  return IterM.mk { stream?, count }

对于该迭代器，文件仍打开时 yield 是合理的，文件已关闭时 done 是合理的。实际的步骤函数会执行读取；若没有返回任何字节，则关闭文件：

instance : Iterator FileIterator IO ByteArray where
  IsPlausibleStep it
    | .yield .. =>
      it.internalState.stream?.isSome
    | .skip .. => False
    | .done => it.internalState.stream?.isNone
  step it := do
    match h : it.internalState.stream? with
    | none => return .deflate <| .done (byit:IterM IO ByteArrayh:it.internalState.stream? = none⊢ match IterStep.done with
| IterStep.yield it_1 out => it.internalState.stream?.isSome = true
| IterStep.skip it => False
| IterStep.done => it.internalState.stream?.isNone = true simp [h]All goals completed! 🐙)
    | some stream =>
      let bytes ← stream.read it.internalState.count
      let it' :=
        { it with internalState.stream? :=
          if bytes.size == 0 then none else some stream
        }
      return .deflate <| .yield it' bytes (byit:IterM IO ByteArraystream:IO.FS.Streamh:it.internalState.stream? = some streambytes:ByteArrayit':IterM IO ByteArray := 
  {
    internalState :=
      let __src := it.internalState;
      { stream? := if (bytes.size == 0) = true then none else some stream, count := __src.count } }⊢ match IterStep.yield it' bytes with
| IterStep.yield it_1 out => it.internalState.stream?.isSome = true
| IterStep.skip it => False
| IterStep.done => it.internalState.stream?.isNone = true simp [h]All goals completed! 🐙)

要在循环中使用它，需要 IteratorLoop 实例。

instance [Monad n] : IteratorLoop FileIterator IO n :=
  .defaultImplementation

这些辅助代码足以使用该迭代器计算文件大小：

def fileSize (name : System.FilePath) : IO Nat := do
  let mut size := 0
  let f := (← iterFile name)
  for bytes in f do
    size := size + bytes.size
  return size

在线查看 ↪

22.2.3. 访问元素🔗

某些迭代器支持高效的随机访问。例如，数组迭代器只需递增其维护的数组索引，即可在常数时间内跳过任意数量的元素。

类型类

Std.IteratorAccess.{w, w'} (α : Type w) (m : Type w → Type w')
  {β : Type w} [Iterator α m β] : Type (max w w')
Std.IteratorAccess.{w, w'} (α : Type w)
  (m : Type w → Type w') {β : Type w}
  [Iterator α m β] : Type (max w w')

IteratorAccess α m 为支持随机访问的迭代器提供高效实现。it.nextAtIdx? n 要么返回 it 发出第 n 个值的步骤（必为 .yield _ _ 形式），要么在 it 尚未发出第 n 个值便终止时返回 .done。

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

此类是实验性的；迭代器 API 的用户不应显式依赖它。

实例构造子

Std.IteratorAccess.mk.{w, w'}

方法

nextAtIdx? : (it : IterM m β) → (n : Nat) → m (PlausibleIterStep (IterM.IsPlausibleNthOutputStep n it))

nextAtIdx? it n 要么返回 it 发出第 n 个值的步骤（必为 .yield _ _ 形式），要么在 it 尚未发出第 n 个值便终止时返回 .done。

定义

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

返回 it 发出第 n 个元素的步骤；若它更早终止，则返回 .done。与 step 不同，此函数一定返回 .yield 或 .done，绝不会返回 .skip 步骤。

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

22.2.4. 循环🔗

类型类

Std.IteratorLoop.{w, w', x, x'} (α : 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')
Std.IteratorLoop.{w, w', x, x'}
  (α : 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 为基于 α 的迭代器提供高效的循环式消费者实现，其基础是一个 ForIn 风格的循环构造。

对良基循环而言，其行为由 LawfulIteratorLoop 类型类完全刻画。

此类是实验性的；迭代器 API 的用户不应显式依赖它。不过，可以假定需要其实例的消费者适用于标准库提供的所有迭代器。

实例构造子

Std.IteratorLoop.mk.{w, w', x, x'}

方法

forIn : ((γ : 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 γ

按 for 循环所期望的方式遍历迭代器 it。

定义

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

这是 IteratorLoop 类的默认实现。它只是使用 IterM.step 遍历迭代器。某些迭代器可以采用更高效的实现，此时应优先使用那些实现。

类型类

Std.LawfulIteratorLoop.{w, w', x, x'} {β : 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
Std.LawfulIteratorLoop.{w, w', x, x'}
  {β : 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

断言给定的 IteratorLoop 实例等于 IteratorLoop.defaultImplementation。（即使二者相等，给定实例也可能高效得多。）

实例构造子

Std.LawfulIteratorLoop.mk.{w, w', x, x'}

方法

lawful : ∀ (lift : (γ : Type w) → (δ : Type x) → (γ → n δ) → m γ → n δ) [Std.Internal.LawfulMonadLiftBindFunction lift]
  (γ : Type x) (it : IterM m β) (init : γ) (Pl : β → γ → ForInStep γ → Prop),
  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

i 中 IteratorLoop.forIn 的实现等于默认实现。

22.2.5. 宇宙层级🔗

为了让迭代器的宇宙层级更加灵活，会在 Iterator.step 的结果外应用包装类型 Shrink。该类型目前只是占位符。它的存在是为了在完整实现可用时缩小破坏性变更的范围。

定义

Std.Shrink.{u} (α : Type u) : Type u
Std.Shrink.{u} (α : Type u) : Type u

目前，Shrink α 只是 α 的包装。

将来，只要有 α 实际上很小的证明，Shrink 应能把 α 缩到可能更小的宇宙，类似 Mathlib 的 Shrink，但后者的转换函数不可计算。在此之前，Shrink α 始终与 α 位于同一宇宙。

这个空操作类型的存在，是为了在真正的 Shrink 类型可用、且迭代器在宇宙方面变得更灵活时，减少破坏性变更。

转换函数 Shrink.deflate 与 Shrink.inflate 在 α 和 Shrink α 之间构成等价，但此等价刻意不是定义等价。

定义

Std.Shrink.inflate.{u_1} {α : Type u_1} (x : Std.Shrink α) : α
Std.Shrink.inflate.{u_1} {α : Type u_1}
  (x : Std.Shrink α) : α

将 Shrink α 的元素转换为 α 的元素。

定义

Std.Shrink.deflate.{u_1} {α : Type u_1} (x : α) : Std.Shrink α
Std.Shrink.deflate.{u_1} {α : Type u_1}
  (x : α) : Std.Shrink α

将 α 的元素转换为 Shrink α 的元素。

22.2.6. 基本迭代器🔗

除了集合类型提供的迭代器，还有两种不与任何底层数据结构关联的基本迭代器。 Iter.empty 不产出任何数据并立即结束迭代，而 Iter.repeat 会永远产出同一元素。这些迭代器主要用作通过组合子构建的更大迭代器的组成部分。

定义

Std.Iter.empty.{w} (β : Type w) : Iter β
Std.Iter.empty.{w} (β : Type w) : Iter β

返回一个立即终止的迭代器。

终止性质：

Finite 实例：总是可用
Productive 实例：总是可用

定义

Std.IterM.empty.{w, w'} (m : Type w → Type w') (β : Type w) : IterM m β
Std.IterM.empty.{w, w'}
  (m : Type w → Type w') (β : Type w) :
  IterM m β

返回一个立即终止的迭代器。

终止性质：

Finite 实例：总是可用
Productive 实例：总是可用

定义

Std.Iter.repeat.{w} {α : Type w} (f : α → α) (init : α) : Iter α
Std.Iter.repeat.{w} {α : Type w}
  (f : α → α) (init : α) : Iter α

由初值 init 和函数 f : α → α 创建一个无限迭代器。它首先发出 init；此后每一步都把 f 应用于前一个值。因此，若刚刚发出了 a，下一步就会发出 f a。换言之，第 n 个值是 Nat.repeat f n init。

例如，若 f := (· + 1) 且 init := 0，迭代器便按顺序发出所有自然数。

终止性质：

Finite 实例：不可用，也绝不可能存在
Productive 实例：总是可用