Lean 语言参考

22.2. 迭代器定义🔗

迭代器可以是单子迭代器或纯迭代器，并且它们可以是有限的、高效的或潜在无限的。 Monadic 迭代器在某些 monad 中使用副作用来发出每个值，因此必须在 monad 中使用，而 pure 迭代器不需要副作用。 例如，迭代目录中的所有文件需要 IO monad。 纯迭代器的类型为 Iter，而一元迭代器的类型为 IterM。

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

An iterator that sequentially emits values of type β. It may be finite or infinite.

See the root module Std.Data.Iterators for a more comprehensive overview over the iterator framework.

See Std.Data.Iterators.Producers for ways to iterate over common data structures. By convention, the monadic iterator associated with an object can be obtained via dot notation. For example, List.iterM IO creates an iterator over a list in the monad IO.

See Init.Data.Iterators.Consumers for ways to use an iterator. For example, it.toList will convert an iterator it into a list and it.ensureTermination.toList guarantees that this operation will terminate, given a proof that the iterator is finite. It is also always possible to manually iterate using it.step, relying on the termination measures it.finitelyManySteps and it.finitelyManySkips.

See IterM for iterators that operate in a monad.

Internally, Iter β wraps an element of type α containing state information. The type α determines the implementation of the iterator using a typeclass mechanism. The concrete typeclass implementing the iterator is Iterator α m β.

When using combinators, α can become very complicated. It is an implicit parameter of α so that the pretty printer will not print this large type by default. If a declaration returns an iterator, the following will not work:

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

Instead the declaration type needs to be completely omitted:

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

-- if you want to ensure that `x` is an iterator emitting `Nat`
def x := ([1, 2, 3].iter : Iter Nat)

Constructor

Std.Iter.mk.{w}

Fields

internalState : α

Internal implementation detail of the iterator.

🔗structure
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

An iterator that sequentially emits values of type β in the monad m. It may be finite or infinite.

See the root module Std.Data.Iterators for a more comprehensive overview over the iterator framework.

See Std.Data.Iterators.Producers for ways to iterate over common data structures. By convention, the monadic iterator associated with an object can be obtained via dot notation. For example, List.iterM IO creates an iterator over a list in the monad IO.

See Init.Data.Iterators.Consumers for ways to use an iterator. For example, it.toList will convert an iterator it into a list and it.ensureTermination.toList guarantees that this operation will terminate, given a proof that the iterator is finite. It is also always possible to manually iterate using it.step, relying on the termination measures it.finitelyManySteps and it.finitelyManySkips.

See Iter for a more convenient interface in case that no monadic effects are needed (m = Id).

Internally, IterM m β wraps an element of type α containing state information. The type α determines the implementation of the iterator using a typeclass mechanism. The concrete typeclass implementing the iterator is Iterator α m β.

When using combinators, α can become very complicated. It is an implicit parameter of α so that the pretty printer will not print this large type by default. If a declaration returns an iterator, the following will not work:

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

Instead the declaration type needs to be completely omitted:

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

-- if you want to ensure that `x` is an iterator in `IO` emitting `Nat`
def x := ([1, 2, 3].iterM IO : IterM IO Nat)

Constructor

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

Wraps the state of an iterator into an Iter object.

Fields

internalState : α

Internal implementation detail of the iterator.

Iter 和 IterM 类型仅仅是内部状态的包装。 该内部状态类型是迭代器类型的隐式参数。 对于基本的生产者迭代器（例如从 List.iter 生成的迭代器），这种类型相当简单；但是，由 combinators 生成的迭代器使用可能会变大的多态状态类型。 由于 Lean 在详细说明函数体之前详细说明了函数的指定返回类型，因此可能无法自动确定函数返回的迭代器类型的内部状态类型。 在这些情况下，从签名中省略返回类型并在定义主体上放置类型注释可能会有所帮助，这允许从主体调用的特定迭代器组合器用于确定状态类型。

Iterator State Types

为列表和数组迭代器显式编写内部状态类型是可行的：

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
Live ↪

迭代的实际过程包括根据请求生成一系列迭代步骤。 每个步骤都会返回一个更新后的迭代器，其中包含新的内部状态以及数据值（以 IterStep.yield 形式）、调用方应再次请求数据值的指示符 (IterStep.skip) 或迭代完成的指示 (IterStep.done)。 如果没有 skip 的能力，那么使用迭代器组合器（例如 Iter.filter）将更加困难，因为这些迭代器组合器不会为底层迭代器生成的所有值生成值。 使用 skip，filter 的实现不需要担心底层迭代器是否是 finite 来成为定义明确的函数，并且可以在单独的证明中进行其有限性的推理。 此外，filter 需要一个内部循环，这对于编译器来说内联要困难得多。

🔗inductive type
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 α β represents a step taken by an iterator (Iter β or IterM m β).

Constructors

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

IterStep.yield it out describes the situation that an iterator emits out and provides it as the succeeding iterator.

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

IterStep.skip it describes the situation that an iterator does not emit anything in this iteration and provides it' as the succeeding iterator.

Allowing skip steps is necessary to generate efficient code from a loop over an iterator.

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

IterStep.done describes the situation that an iterator has finished and will neither emit more values nor cause any monadic effects. In this case, no succeeding iterator is provided.

Iter 和 IterM 采取的步骤分别由类型 Iter.Step 和 IterM.Step 表示。 两种类型的步骤都是 IterStep 的包装器，其中包括用于跟踪终止行为的 附加证明。

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

The type of the step object returned by Iter.step, containing an IterStep and a proof that this is a plausible step for the given iterator.

🔗def
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

The type of the step object returned by IterM.step, containing an IterStep and a proof that this is a plausible step for the given iterator.

步骤是使用 Iterator.step（Iterator 类型类的方法）的迭代器生成的。 Iterator 用于纯迭代器和一元迭代器；纯迭代器在 monad 的选择上可以是完全多态的，这允许调用者使用 Id 实例化它。

🔗type class
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')

The step function of an iterator in Iter (α := α) β or IterM (α := α) m β.

In order to allow intrinsic termination proofs when iterating with the step function, the step object is bundled with a proof that it is a "plausible" step for the given current iterator.

Instance Constructor

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

Methods

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

A relation that governs the allowed steps from a given iterator.

The "plausible" steps are those which make sense for a given state; plausibility can ensure properties such as the successor iterator being drawn from the same collection, that an iterator resulting from a skip will return the same next value, or that the next item yielded is next one in the original collection.

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

Carries out a step of iteration.

22.2.1. 合理性🔗

除了阶跃函数之外，Iterator 的实例还包括关系 Iterator.IsPlausibleStep。 这种关系的存在是因为大多数迭代器都保持其内部状态的不变性并以可预测的方式产生值。 例如，数组迭代器跟踪数组和数组中的当前索引。 步进数组迭代器会导致迭代器遍历相同的底层数组；当索引足够小时，它会产生一个值，否则会产生一个值。 迭代器状态中的 plausible Steps 是通过 IsPlausibleStep 的迭代器实现与其相关的那些步骤。 在逻辑级别跟踪合理性使得推断单子迭代器的终止行为变得可行。

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

🔗def
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)

A variant of IterStep that bundles the step together with a proof that it is "plausible". The plausibility predicate will later be chosen to assert that a state is a plausible successor of another state. Having this proof bundled up with the step is important for termination proofs.

See IterM.Step and Iter.Step for the concrete choice of the plausibility predicate.

🔗def
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

Match pattern for the yield case. See also IterStep.yield.

🔗def
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

Match pattern for the skip case. See also IterStep.skip.

🔗def
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

Match pattern for the done case. See also IterStep.done.

22.2.2. 有限且高效的迭代器🔗

并非所有迭代器都保证返回有限数量的结果；迭代所有自然数是完全明智的。 同样，并非所有迭代器都保证返回单个结果或终止；迭代器可以使用任意程序定义。 因此，Lean 将迭代器分为三个终止类：

  • Finite 迭代器保证在有限数量的步骤后完成迭代。这些迭代器有一个 Finite 实例。

  • Productive 迭代器保证在有限多个步骤中产生一个值或终止，但它们可能产生无限多个值。这些迭代器有一个 Productive 实例。

  • 所有其他迭代器，其终止行为未知。这些迭代器都没有实例。

所有有限迭代器都必然是高效的。

🔗type class
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 asserts that IterM (α := α) m terminates after finitely many steps. Technically, this means that the relation of plausible successors is well-founded. Given this typeclass, termination proofs for well-founded recursion over an iterator it can use it.finitelyManySteps as a termination measure.

Instance Constructor

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

Methods

wf : WellFounded IterM.IsPlausibleSuccessorOf

The relation of plausible successors is well-founded.

🔗type class
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 asserts that IterM (α := α) m terminates or emits a value after finitely many skips. Technically, this means that the relation of plausible successors during skips is well-founded. Given this typeclass, termination proofs for well-founded recursion over an iterator it can use it.finitelyManySkips as a termination measure.

Instance Constructor

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

Methods

wf : WellFounded IterM.IsPlausibleSkipSuccessorOf

The relation of plausible successors during skips is well-founded.

Lean 的标准库提供了许多迭代迭代器的函数。这些消费者功能通常不 对底层迭代器做出任何假设。特别是，对于某些迭代器，此类函数可能会永远运行。

有时，函数确实终止是至关重要的。 对于这些情况，组合器 Iter.ensureTermination 会产生一个迭代器，该迭代器提供保证终止的消费者变体。 他们通常需要证明所涉及的迭代器是有限的。

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

For an iterator it, it.ensureTermination provides variants of consumers that always terminate.

🔗def
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 β

For an iterator it, it.ensureTermination provides variants of consumers that always terminate.

Iterating Over Nat

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

structure Nats where next : Nat

该迭代器只会产生下一个自然数。 因此，其步进函数永远不会返回 skip 或 done。 每当它产生一个值时，该值将是内部状态的 next 字段，并且后继迭代器的 next 字段将大 1。 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 (m: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 All 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 for 'for_in%' notation ForIn (EIO IO.Error) (Iter.Total Nat) ?m.12for x in Nats.iter.ensureTermination do IO.println s!"{x}" 
failed to synthesize instance for 'for_in%' notation
  ForIn (EIO IO.Error) (Iter.Total Nat) ?m.12
Live ↪
Iterating Over Triples

类型 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 All goals completed! 🐙

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

def abc : Triple Char := ⟨'a', 'b', 'c'⟩ #['a', 'b', 'c']#eval abc.iter.toArray 
#['a', 'b', 'c']

一般来说，Iter.toArray 可能会永远运行。可以证明 abc 是有限的，上面的例子将在有限多个步骤后终止，通过 构造 Finite (Triple Char) Id 实例。 最简单的方法是从 TriplePos.done 开始，向后推向 TriplePos.fst，从而显示每个位置依次具有有限的后继链：

@[grind! .] theorem acc_done [Pure m] : Acc (IterM.IsPlausibleSuccessorOf (m := m)) ⟨{ triple, pos := .done : TripleIterator α}⟩ := Acc.intro _ fun 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✝ 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✝ m: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✝m: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✝ m: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✝m: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✝ All goals completed! 🐙 @[grind! .] theorem acc_thd [Pure m] : Acc (IterM.IsPlausibleSuccessorOf (m := m)) ⟨{ triple, pos := .thd : TripleIterator α}⟩ := Acc.intro _ fun 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 } } 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 } } m: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 } }m: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 } } m: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 } }m: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 } } All goals completed! 🐙 @[grind! .] theorem acc_snd [Pure m] : Acc (IterM.IsPlausibleSuccessorOf (m := m)) ⟨{ triple, pos := .snd : TripleIterator α}⟩ := Acc.intro _ fun 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 } } 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 } } m: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 } }m: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 } } m: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 } }m: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 } } All goals completed! 🐙 @[grind! .] theorem acc_fst [Pure m] : Acc (IterM.IsPlausibleSuccessorOf (m := m)) ⟨{ triple, pos := .fst : TripleIterator α}⟩ := Acc.intro _ fun 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 } } 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 } } m: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 } }m: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 } } m: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 } }m: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 } } All goals completed! 🐙 instance [Pure m] : Finite (TripleIterator α) m where wf := .intro <| fun m:Type u_1 → Type u_2α:Type u_1inst✝:Pure mtriple:Triple αpos:TriplePos⊢ Acc IterM.IsPlausibleSuccessorOf { internalState := { triple := triple, pos := pos } } m:Type u_1 → Type u_2α:Type u_1inst✝:Pure mtriple:Triple αpos:TriplePos⊢ Acc IterM.IsPlausibleSuccessorOf { internalState := { triple := triple, pos := pos } } m:Type u_1 → Type u_2α:Type u_1inst✝:Pure mtriple:Triple α⊢ Acc IterM.IsPlausibleSuccessorOf { internalState := { triple := triple, pos := TriplePos.fst } }m:Type u_1 → Type u_2α:Type u_1inst✝:Pure mtriple:Triple α⊢ Acc IterM.IsPlausibleSuccessorOf { internalState := { triple := triple, pos := TriplePos.snd } }m:Type u_1 → Type u_2α:Type u_1inst✝:Pure mtriple:Triple α⊢ Acc IterM.IsPlausibleSuccessorOf { internalState := { triple := triple, pos := TriplePos.thd } }m:Type u_1 → Type u_2α:Type u_1inst✝:Pure mtriple:Triple α⊢ Acc IterM.IsPlausibleSuccessorOf { internalState := { triple := triple, pos := TriplePos.done } } m:Type u_1 → Type u_2α:Type u_1inst✝:Pure mtriple:Triple α⊢ Acc IterM.IsPlausibleSuccessorOf { internalState := { triple := triple, pos := TriplePos.fst } }m:Type u_1 → Type u_2α:Type u_1inst✝:Pure mtriple:Triple α⊢ Acc IterM.IsPlausibleSuccessorOf { internalState := { triple := triple, pos := TriplePos.snd } }m:Type u_1 → Type u_2α:Type u_1inst✝:Pure mtriple:Triple α⊢ Acc IterM.IsPlausibleSuccessorOf { internalState := { triple := triple, pos := TriplePos.thd } }m:Type u_1 → Type u_2α:Type u_1inst✝:Pure mtriple:Triple α⊢ Acc IterM.IsPlausibleSuccessorOf { internalState := { triple := triple, pos := TriplePos.done } } All goals completed! 🐙

要在 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 循环中启用迭代器，需要 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
Live ↪
Iterators and Effects

迭代文件内容的一种方法是在每一步从 Stream 读取指定数量的字节。 当到达 EOF 时，迭代器可以通过让其引用计数降至零来关闭文件：

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 let { stream?, count } := it.internalState match stream? with | none => return .deflate <| .done rfl | some stream => let bytes ← stream.read count let it' := { it with internalState.stream? := if bytes.size == 0 then none else some stream } return .deflate <| .yield it' bytes (it:IterM IO ByteArraystream?:Option IO.FS.Streamcount:USizestream:IO.FS.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 out => { stream? := some stream, count := count }.stream?.isSome = true | IterStep.skip it => False | IterStep.done => { stream? := some stream, count := count }.stream?.isNone = true 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
Live ↪

22.2.3. 访问元素🔗

一些迭代器支持高效的随机访问。 例如，数组迭代器可以通过增加其在数组中维护的索引来在恒定时间内跳过任意数量的元素。

🔗type class
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 provides efficient implementations for random access or iterators that support it. it.nextAtIdx? n either returns the step in which the nth value of it is emitted (necessarily of the form .yield _ _) or .done if it terminates before emitting the nth value.

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

This class is experimental and users of the iterator API should not explicitly depend on it.

Instance Constructor

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

Methods

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

nextAtIdx? it n either returns the step in which the nth value of it is emitted (necessarily of the form .yield _ _) or .done if it terminates before emitting the nth value.

🔗def
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))

Returns the step in which it yields its n-th element, or .done if it terminates earlier. In contrast to step, this function will always return either .yield or .done but never a .skip step.

For monadic iterators, the monadic effects of this operation may differ from manually iterating to the n-th value because nextAtIdx? 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.

22.2.4. 循环🔗

🔗type class
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 provides efficient implementations of loop-based consumers for α-based iterators. The basis is a ForIn-style loop construct.

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

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

Instance Constructor

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

Methods

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 γ

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

🔗def
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

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.

🔗type class
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

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

Instance Constructor

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

Methods

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

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

22.2.5. 宇宙层级🔗

为了使迭代器的 宇宙层级 更加灵活，在 Iterator.step 的结果周围应用了包装类型 Shrink。 该类型目前是占位符。 当完整实施可用时，它的存在是为了减少重大变更的范围。

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

Currently, Shrink α is just a wrapper around α.

In the future, Shrink should allow shrinking α into a potentially smaller universe, given a proof that α is actually small, just like Mathlib's Shrink, except that the latter's conversion functions are noncomputable. Until then, Shrink α is always in the same universe as α.

This no-op type exists so that fewer breaking changes will be needed when the real Shrink type is available and the iterators will be made more flexible with regard to universes.

The conversion functions Shrink.deflate and Shrink.inflate form an equivalence between α and Shrink α, but this equivalence is intentionally not definitional.

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

Converts elements of Shrink α into elements of α.

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

Converts elements of α into elements of Shrink α.

22.2.6. 基本迭代器🔗

除了集合类型提供的迭代器之外，还有两个不连接到任何底层数据结构的基本迭代器。 Iter.empty 在没有产生任何数据后立即完成迭代，并且 Iter.repeat 永远产生相同的元素。 这些迭代器主要用作使用组合器构建的大型迭代器的一部分。

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

Returns an iterator that terminates immediately.

Termination properties:

🔗def
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 β

Returns an iterator that terminates immediately.

Termination properties:

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

Creates an infinite iterator from an initial value init and a function f : α → α. First it yields init, and in each successive step, the iterator applies f to the previous value. So if the iterator just emitted a, in the next step it will yield f a. In other words, the n-th value is Nat.repeat f n init.

For example, if f := (· + 1) and init := 0, then the iterator emits all natural numbers in order.

Termination properties: