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

将迭代器的状态包装成 Iter 对象。

Std.Iter.toIterM.{w} {α β : Type w} (it : Iter β) : IterM Id β
Std.Iter.toIterM.{w} {α β : Type w}
  (it : Iter β) : IterM Id β

把纯迭代器（Iter β）转换为恒等单子 Id 中的单子式迭代器（IterM Id β）。

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

给定迭代器 it 和自然数 n，it.take n 会按顺序输出 it 最前面的至多 n 个值，然后终止。

弹珠图：

it ---a----b---c--d-e--⊥ it.take 3 ---a----b---c⊥ it ---a--⊥ it.take 3 ---a--⊥

终止性质：

• Finite 实例：仅当 it 能产时可用

• Productive 实例：仅当 it 能产时可用

性能：

it 每发出一个值，此组合子都会引入额外 O(1) 开销。

Std.Iter.takeWhile.{w} {α β : Type w} (P : β → Bool) (it : Iter β) :
  Iter β
Std.Iter.takeWhile.{w} {α β : Type w}
  (P : β → Bool) (it : Iter β) : Iter β

给定迭代器 it 和谓词 P，it.takeWhile P 会输出 it 发出的值，直到其中一个值被 P 拒绝。若某个发出的值被 P 拒绝，该值会被丢弃，迭代器随即终止。

弹珠图：

假设谓词 P 接受 a 和 b，但拒绝 c：

it ---a----b---c--d-e--⊥ it.takeWhile P ---a----b---⊥ it ---a----⊥ it.takeWhile P ---a----⊥

终止性质：

• Finite 实例：仅当 it 有限时可用

• Productive 实例：仅当 it 能产时可用

视 P 而定，即使 it 并非有限（或能产），it.takeWhile P 也可能有限（或能产）。此时需要手动证明 Finite（或 Productive）实例。

性能：

此组合子对 it 的每个输出调用 P，直到谓词求值为假，随后终止。

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

此组合子只适用于高级用例。

给定有限迭代器 it，返回一个行为与 it 完全相同、但类型与 it.take n 相同的迭代器。

弹珠图：

it ---a----b---c--d-e--⊥ it.toTake ---a----b---c--d-e--⊥

终止性质：

• Finite 实例：总是可用

• Productive 实例：总是可用

性能：

it 每发出一个值，此组合子都会引入额外 O(1) 开销。

Std.Iter.drop.{w} {α β : Type w} (n : Nat) (it : Iter β) : Iter β
Std.Iter.drop.{w} {α β : Type w} (n : Nat)
  (it : Iter β) : Iter β

给定迭代器 it 和自然数 n，it.drop n 会转发 it 除前 n 个之外的所有输出值。

弹珠图：

it ---a----b---c--d-e--⊥ it.drop 3 ---------------d-e--⊥ it ---a--⊥ it.drop 3 ------⊥

终止性质：

• Finite 实例：仅当 it 有限时可用

• Productive 实例：仅当 it 能产时可用

性能：

目前，即使迭代器已不再丢弃任何元素，it 每发出一个值，此组合子仍会引入额外 O(1) 开销。

Std.Iter.dropWhile.{w} {α β : Type w} (P : β → Bool) (it : Iter β) :
  Iter β
Std.Iter.dropWhile.{w} {α β : Type w}
  (P : β → Bool) (it : Iter β) : Iter β

给定迭代器 it 和谓词 P，it.dropWhile P 会从第一个被 P 拒绝的值开始，发出 it 所发出的值；此前的元素都被丢弃。

若 P 是单子式的，请改用 dropWhileM。

弹珠图：

假设谓词 P 接受 a 和 b，但拒绝 c：

it ---a----b---c--d-e--⊥ it.dropWhile P ------------c--d-e--⊥ it ---a----⊥ it.dropWhile P --------⊥

终止性质：

• Finite 实例：仅当 it 有限时可用

• Productive 实例：仅当 it 有限时可用

视 P 而定，即使 it 不能产，it.dropWhileM P 也可能能产。此时需要手动证明 Productive 实例。

性能：

此组合子对 it 的每个输出调用 P，直到谓词求值为假。此后，it 每发出一个值，组合子都会引入额外 O(1) 开销。

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

生成一个迭代器：先发出 it 的一个值，再丢弃 n - 1 个元素，然后再发出一个值，如此继续。换言之，它从第一个值开始，每隔 n 个值发出一个 it 的值。

若 n = 0，迭代器的行为与 n = 1 时相同：发出 it 的所有值。

弹珠图：

it ---1----2----3---4----5 it.stepSize 2 ---1---------3--------5

可用性：

此操作目前仅适用于实现 IteratorAccess 的迭代器，例如 PRange.iter 范围迭代器。

终止性质：

• Finite 实例：仅当基础迭代器 it 有限时可用

• Productive 实例：总是可用

Std.Iter.map.{w} {α β γ : Type w} [Iterator α Id β] (f : β → γ)
  (it : Iter β) : Iter γ
Std.Iter.map.{w} {α β γ : Type w}
  [Iterator α Id β] (f : β → γ)
  (it : Iter β) : Iter γ

若 it 是迭代器，则 it.map f 是另一个迭代器：它把函数 f 应用于 it 发出的所有值，并发出结果。

若 f 是单子式的，请改用 mapM。

弹珠图：

it ---a --b --c --d -e ----⊥ it.map ---a'--b'--c'--d'-e'----⊥

（其中 f a = a'、f b = b'，依此类推。）

终止性质：

• Finite 实例：仅当 it 有限时可用

• Productive 实例：仅当 it 能产时可用

性能：

基础迭代器 it 每发出一个值，此组合子都会调用 f。

Std.Iter.mapM.{w, w'} {α β γ : Type w} [Iterator α Id β]
  {m : Type w → Type w'} [Monad m] [MonadAttach m] (f : β → m γ)
  (it : Iter β) : IterM m γ
Std.Iter.mapM.{w, w'} {α β γ : Type w}
  [Iterator α Id β] {m : Type w → Type w'}
  [Monad m] [MonadAttach m] (f : β → m γ)
  (it : Iter β) : IterM m γ

若 it 是迭代器，则 it.mapM f 是另一个迭代器：它把单子式函数 f 应用于 it 发出的所有值，并发出结果。

基础迭代器 it 位于单子 m 中；只要有 MonadLiftT m n 实例，f 就可在任意单子 n 中返回值。

若 f 是纯函数，可改用更简单的 it.map。

弹珠图（忽略单子式效应）：

it ---a --b --c --d -e ----⊥ it.mapM ---a'--b'--c'--d'-e'----⊥

（其中 f a = pure a'、f b = pure b'，依此类推。）

终止性质：

• Finite 实例：仅当 it 有限时可用

• Productive 实例：仅当 it 能产时可用

对某些映射函数 f，即使没有提供 Finite（或 Productive）实例，所得迭代器仍会有限（或能产）。例如，若 f 位于 ExceptT 单子中且总会失败，则即使 it 不有限，it.mapM 也会有限。此时需要手动完成终止性证明。

性能：

基础迭代器 it 每发出一个值，此组合子都会调用 f。

Std.Iter.mapWithPostcondition.{w, w'} {α β γ : Type w} [Iterator α Id β]
  {m : Type w → Type w'} [Monad m] (f : β → PostconditionT m γ)
  (it : Iter β) : IterM m γ
Std.Iter.mapWithPostcondition.{w, w'}
  {α β γ : Type w} [Iterator α Id β]
  {m : Type w → Type w'} [Monad m]
  (f : β → PostconditionT m γ)
  (it : Iter β) : IterM m γ

注意：这是一个非常通用的组合子，需要深入理解单子、依赖类型和终止性证明。变体 map 与 mapM 更易使用，足以满足大多数用例。

若 it 是迭代器，则 it.mapWithPostcondition f 是另一个迭代器：它把单子式函数 f 应用于 it 发出的所有值，并发出结果。

f 应返回 PostconditionT n _，其中 n 是任意单子。PostconditionT 变换器让调用者能在单子 n 中内蕴地证明关于 f 返回值的性质，从而可以依据 f 的具体行为证明终止。

弹珠图（忽略单子式效应）：

it ---a --b --c --d -e ----⊥ it.mapWithPostcondition ---a'--b'--c'--d'-e'----⊥

（其中 f a = pure a'、f b = pure b'，依此类推。）

终止性质：

• Finite 实例：仅当 it 有限时可用

• Productive 实例：仅当 it 能产时可用

对某些映射函数 f，即使没有提供 Finite（或 Productive）实例，所得迭代器仍会有限（或能产）。例如，若 f 位于 ExceptT 单子中且总会失败，则即使 it 不有限，it.mapWithPostcondition 也会有限。

在这种情况下，只要 PostconditionT n 单子中携带的后置条件足够强，就能手动证明缺失的实例。在上述例子中，合适的后置条件可以是 fun _ => False。

性能：

基础迭代器 it 每发出一个值，此组合子都会调用 f。

Std.Iter.uLift.{v, u} {α β : Type u} (it : Iter β) : Iter (ULift β)
Std.Iter.uLift.{v, u} {α β : Type u}
  (it : Iter β) : Iter (ULift β)

把值位于 β 的迭代器转换为值位于 ULift β 的迭代器。

map 等多数其他组合子无法跨越宇宙层级；此组合子可用于过渡到更高宇宙。

弹珠图：

it ---a ----b ---c --d ---⊥ it.uLift n ---.up a----.up b---.up c--.up d---⊥

终止性质：

• Finite：仅当原迭代器有限时可用

• Productive：仅当原迭代器能产时可用

Std.Iter.flatMap.{w} {α β α₂ γ : Type w} [Iterator α Id β]
  [Iterator α₂ Id γ] (f : β → Iter γ) (it : Iter β) : Iter γ
Std.Iter.flatMap.{w} {α β α₂ γ : Type w}
  [Iterator α Id β] [Iterator α₂ Id γ]
  (f : β → Iter γ) (it : Iter β) : Iter γ

设 it 为迭代器，f 为把 it 的输出映射到迭代器的函数。it.flatMap f 遍历 it，对每个输出应用 f，再遍历所得迭代器。it.flatMap f 会发出内部迭代器得到的全部值：先发出第一个内部迭代器的所有值，再发出第二个的所有值，依此类推。

弹珠图：

it                 ---a      --b      c    --d -⊥
f a                    a1-a2⊥
f b                             b1-b2⊥
f c                                    c1-c2⊥
f d                                           ⊥
it.flatMap         ----a1-a2----b1-b2--c1-c2----⊥

终止性质：

• Finite 实例：仅当 it 和内部迭代器都有限时可用

• Productive 实例：仅当 it 有限且内部迭代器能产时可用

对某些函数 f，即使没有现成的 Finite（或 Productive）实例，所得迭代器仍会有限（或能产）。例如，若外部迭代器能产，且内部迭代器能产并且可证明绝不为空，则所得迭代器也能产。

性能：

it 或内部迭代器每发出一个值，此组合子都会引入额外 O(1) 开销。

外部迭代器 it 每发出一个值，此组合子都会调用 f。

Std.Iter.flatMapM.{w, w'} {α β α₂ γ : Type w} {m : Type w → Type w'}
  [Monad m] [MonadAttach m] [Iterator α Id β] [Iterator α₂ m γ]
  (f : β → m (IterM m γ)) (it : Iter β) : IterM m γ
Std.Iter.flatMapM.{w, w'}
  {α β α₂ γ : Type w}
  {m : Type w → Type w'} [Monad m]
  [MonadAttach m] [Iterator α Id β]
  [Iterator α₂ m γ]
  (f : β → m (IterM m γ)) (it : Iter β) :
  IterM m γ

设 it 为迭代器，f 为单子式的、把 it 的输出映射到迭代器的函数。it.flatMapM f 遍历 it，对每个输出应用 f，再遍历所得迭代器。it.flatMapM f 会发出内部迭代器得到的全部值：先发出第一个内部迭代器的所有值，再发出第二个的所有值，依此类推。

弹珠图（忽略单子式效应）：

it                 ---a      --b      c    --d -⊥
f a                    a1-a2⊥
f b                             b1-b2⊥
f c                                    c1-c2⊥
f d                                           ⊥
it.flatMapM        ----a1-a2----b1-b2--c1-c2----⊥

终止性质：

• Finite 实例：仅当 it 和内部迭代器都有限时可用

• Productive 实例：仅当 it 有限且内部迭代器能产时可用

对某些函数 f，即使没有现成的 Finite（或 Productive）实例，所得迭代器仍会有限（或能产）。例如，若外部迭代器能产，且内部迭代器能产并且可证明绝不为空，则所得迭代器也能产。

性能：

it 或内部迭代器每发出一个值，此组合子都会引入额外 O(1) 开销。

外部迭代器 it 每发出一个值，此组合子都会调用 f。

Std.Iter.flatMapAfter.{w} {α β α₂ γ : Type w} [Iterator α Id β]
  [Iterator α₂ Id γ] (f : β → Iter γ) (it₁ : Iter β)
  (it₂ : Option (Iter γ)) : Iter γ
Std.Iter.flatMapAfter.{w}
  {α β α₂ γ : Type w} [Iterator α Id β]
  [Iterator α₂ Id γ] (f : β → Iter γ)
  (it₁ : Iter β) (it₂ : Option (Iter γ)) :
  Iter γ

设 it₁ 和 it₂ 为迭代器，f 为把 it₁ 的输出映射到与 it₂ 同类型迭代器的函数。it₁.flatMapAfter f it₂ 先遍历 it₂，然后遍历 it₁.flatMap f it₂，并发出二者的全部值。

此组合子的主要用途，是表示一个 flatMap 迭代器正在遍历某个内部迭代器时的中间状态。

弹珠图：

it₁                            --b      c    --d -⊥
it₂                      a1-a2⊥
f b                               b1-b2⊥
f c                                      c1-c2⊥
f d                                             ⊥
it.flatMapAfter  f it₂   a1-a2----b1-b2--c1-c2----⊥

终止性质：

• Finite 实例：仅当 it₁、it₂ 和内部迭代器都有限时可用

• Productive 实例：仅当 it₁ 有限，且 it₂ 和内部迭代器能产时可用

对某些函数 f，即使没有现成的 Finite（或 Productive）实例，所得迭代器仍会有限（或能产）。例如，若外部迭代器能产，且内部迭代器能产并且可证明绝不为空，则所得迭代器也能产。

性能：

it₁、it₂ 或内部迭代器每发出一个值，此组合子都会引入额外 O(1) 开销。

外部迭代器 it₁ 每发出一个值，此组合子都会调用 f。

Std.Iter.flatMapAfterM.{w, w'} {α β α₂ γ : Type w}
  {m : Type w → Type w'} [Monad m] [MonadAttach m] [Iterator α Id β]
  [Iterator α₂ m γ] (f : β → m (IterM m γ)) (it₁ : Iter β)
  (it₂ : Option (IterM m γ)) : IterM m γ
Std.Iter.flatMapAfterM.{w, w'}
  {α β α₂ γ : Type w}
  {m : Type w → Type w'} [Monad m]
  [MonadAttach m] [Iterator α Id β]
  [Iterator α₂ m γ]
  (f : β → m (IterM m γ)) (it₁ : Iter β)
  (it₂ : Option (IterM m γ)) : IterM m γ

设 it₁ 和 it₂ 为迭代器，f 为单子式的、把 it₁ 的输出映射到与 it₂ 同类型迭代器的函数。it₁.flatMapAfterM f it₂ 先遍历 it₂，然后遍历 it₁.flatMap f it₂，并发出二者的全部值。

此组合子的主要用途，是表示一个 flatMap 迭代器正在遍历某个内部迭代器时的中间状态。

弹珠图（忽略单子式效应）：

it₁                            --b      c    --d -⊥
it₂                      a1-a2⊥
f b                               b1-b2⊥
f c                                      c1-c2⊥
f d                                             ⊥
it.flatMapAfterM f it₂   a1-a2----b1-b2--c1-c2----⊥

终止性质：

• Finite 实例：仅当 it₁、it₂ 和内部迭代器都有限时可用

• Productive 实例：仅当 it₁ 有限，且 it₂ 和内部迭代器能产时可用

对某些函数 f，即使没有现成的 Finite（或 Productive）实例，所得迭代器仍会有限（或能产）。例如，若外部迭代器能产，且内部迭代器能产并且可证明绝不为空，则所得迭代器也能产。

性能：

it₁、it₂ 或内部迭代器每发出一个值，此组合子都会引入额外 O(1) 开销。

外部迭代器 it₁ 每发出一个值，此组合子都会调用 f。

Std.Iter.filter.{w} {α β : Type w} [Iterator α Id β] (f : β → Bool)
  (it : Iter β) : Iter β
Std.Iter.filter.{w} {α β : Type w}
  [Iterator α Id β] (f : β → Bool)
  (it : Iter β) : Iter β

若 it 是迭代器，则 it.filter f 是另一个迭代器：它把谓词 f 应用于 it 发出的所有值，并且只发出被 f 接受的值。

若 f 是单子式的，请改用 filterM。

弹珠图（忽略单子式效应）：

it ---a--b--c--d-e--⊥ it.filter ---a-----c-------⊥

（其中 f a = f c = true，且 f b = f d = d e = false。）

终止性质：

• Finite 实例：仅当 it 有限时可用

• Productive 实例：仅当 it 有限时可用

对某些映射函数 f，即使没有提供 Productive 实例，所得迭代器仍会能产。例如，若 f 总是返回 True，则只要 it 能产，所得迭代器也能产。此时需要手动证明缺失的实例。

性能：

基础迭代器 it 每发出一个值，此组合子都会调用 f，并对返回值进行模式匹配。

Std.Iter.filterM.{w, w'} {α β : Type w} [Iterator α Id β]
  {m : Type w → Type w'} [Monad m] [MonadAttach m]
  (f : β → m (ULift Bool)) (it : Iter β) : IterM m β
Std.Iter.filterM.{w, w'} {α β : Type w}
  [Iterator α Id β] {m : Type w → Type w'}
  [Monad m] [MonadAttach m]
  (f : β → m (ULift Bool)) (it : Iter β) :
  IterM m β

若 it 是迭代器，则 it.filterM f 是另一个迭代器：它把单子式谓词 f 应用于 it 发出的所有值，并且只发出被 f 接受的值。

若 f 是纯函数，可改用更简单的 it.filter。

弹珠图（忽略单子式效应）：

it ---a--b--c--d-e--⊥ it.filterM ---a-----c-------⊥

（其中 f a = f c = pure true，且 f b = f d = d e = pure false。）

终止性质：

• Finite 实例：仅当 it 有限时可用

• Productive 实例：仅当 it 有限时可用

对某些映射函数 f，即使没有提供 Finite（或 Productive）实例，所得迭代器仍会有限（或能产）。例如，若 f 位于 ExceptT 单子中且总会失败，则即使 it 不有限，it.filterWithPostcondition 也会有限并且能产。此时需要手动完成终止性证明。

性能：

基础迭代器 it 每发出一个值，此组合子都会调用 f。

Std.Iter.filterWithPostcondition.{w, w'} {α β : Type w}
  [Iterator α Id β] {m : Type w → Type w'} [Monad m]
  (f : β → PostconditionT m (ULift Bool)) (it : Iter β) : IterM m β
Std.Iter.filterWithPostcondition.{w, w'}
  {α β : Type w} [Iterator α Id β]
  {m : Type w → Type w'} [Monad m]
  (f : β → PostconditionT m (ULift Bool))
  (it : Iter β) : IterM m β

注意：这是一个非常通用的组合子，需要深入理解单子、依赖类型和终止性证明。变体 filter 与 filterM 更易使用，足以满足大多数用例。

若 it 是迭代器，则 it.filterWithPostcondition f 是另一个迭代器：它把单子式谓词 f 应用于 it 发出的所有值，并且只发出被 f 接受的值。

f 应返回 PostconditionT n (ULift Bool)，其中 n 是任意单子。PostconditionT 变换器让调用者能在单子 n 中内蕴地证明关于 f 返回值的性质，从而可以依据 f 的具体行为证明终止。

弹珠图（忽略单子式效应）：

it ---a--b--c--d-e--⊥ it.filterWithPostcondition ---a-----c-------⊥

（其中 f a = f c = pure true，且 f b = f d = d e = pure false。）

终止性质：

• Finite 实例：仅当 it 有限时可用

• Productive 实例：仅当 it 有限时可用

对某些映射函数 f，即使没有提供 Finite（或 Productive）实例，所得迭代器仍会有限（或能产）。例如，若 f 位于 ExceptT 单子中且总会失败，则即使 it 不有限，it.filterWithPostcondition 也会有限并且能产。

在这种情况下，只要 PostconditionT n 单子中携带的后置条件足够强，就能手动证明缺失的实例。在上述例子中，合适的后置条件可以是 fun _ => False。

性能：

基础迭代器 it 每发出一个值，此组合子都会调用 f。

Std.Iter.filterMap.{w} {α β γ : Type w} [Iterator α Id β]
  (f : β → Option γ) (it : Iter β) : Iter γ
Std.Iter.filterMap.{w} {α β γ : Type w}
  [Iterator α Id β] (f : β → Option γ)
  (it : Iter β) : Iter γ

若 it 是迭代器，则 it.filterMap f 是另一个迭代器：它把函数 f 应用于 it 发出的所有值。f 应返回一个 Option。若返回 none，则不发出任何值；若返回 some x，则发出 x。

若 f 是单子式的，请改用 filterMapM。

弹珠图：

it ---a --b--c --d-e--⊥ it.filterMap ---a'-----c'-------⊥

（其中 f a = some a'、f c = c'，且 f b = f d = d e = none。）

终止性质：

• Finite 实例：仅当 it 有限时可用

• Productive 实例：仅当 it 有限时可用

对某些映射函数 f，即使没有提供 Productive 实例，所得迭代器仍会能产。例如，若 f 从不返回 none，此组合子便会保持能产性。此时需要手动证明缺失的实例。

性能：

基础迭代器 it 每发出一个值，此组合子都会调用 f，并对返回的 Option 值进行模式匹配。

Std.Iter.filterMapM.{w, w'} {α β γ : Type w} [Iterator α Id β]
  {m : Type w → Type w'} [Monad m] [MonadAttach m]
  (f : β → m (Option γ)) (it : Iter β) : IterM m γ
Std.Iter.filterMapM.{w, w'}
  {α β γ : Type w} [Iterator α Id β]
  {m : Type w → Type w'} [Monad m]
  [MonadAttach m] (f : β → m (Option γ))
  (it : Iter β) : IterM m γ

若 it 是迭代器，则 it.filterMapM f 是另一个迭代器：它把单子式函数 f 应用于 it 发出的所有值。f 应返回单子中的 Option。若 f 返回 none，则不发出任何值；若返回 some x，则发出 x。

若 f 是纯函数，可改用更简单的 it.filterMap。

弹珠图（忽略单子式效应）：

it ---a --b--c --d-e--⊥ it.filterMapM ---a'-----c'-------⊥

（其中 f a = pure (some a)'、f c = pure (some c')，且 f b = f d = d e = pure none。）

终止性质：

• Finite 实例：仅当 it 有限时可用

• Productive 实例：仅当 it 有限时可用

对某些映射函数 f，即使没有提供 Finite（或 Productive）实例，所得迭代器仍会有限（或能产）。例如，若 f 从不返回 none，此组合子便保持能产性；若 f 位于 ExceptT 单子中且总会失败，则即使 it 不有限，it.filterMapM 也会有限。此时需要手动完成终止性证明。

性能：

基础迭代器 it 每发出一个值，此组合子都会调用 f，并对返回的 Option 值进行模式匹配。

Std.Iter.filterMapWithPostcondition.{w, w'} {α β γ : Type w}
  [Iterator α Id β] {m : Type w → Type w'} [Monad m]
  (f : β → PostconditionT m (Option γ)) (it : Iter β) : IterM m γ
Std.Iter.filterMapWithPostcondition.{w,
    w'}
  {α β γ : Type w} [Iterator α Id β]
  {m : Type w → Type w'} [Monad m]
  (f : β → PostconditionT m (Option γ))
  (it : Iter β) : IterM m γ

注意：这是一个非常通用的组合子，需要深入理解单子、依赖类型和终止性证明。变体 filterMap 与 filterMapM 更易使用，足以满足大多数用例。

若 it 是迭代器，则 it.filterMapWithPostcondition f 是另一个迭代器：它把单子式函数 f 应用于 it 发出的所有值。f 应在单子中返回一个 Option。若 f 返回 none，则不发出任何值；若返回 some x，则发出 x。

f 应返回 PostconditionT n (Option _)，其中 n 是任意单子。PostconditionT 变换器让调用者能在单子 n 中内蕴地证明关于 f 返回值的性质，从而可以依据 f 的具体行为证明终止。

弹珠图（忽略单子式效应）：

it ---a --b--c --d-e--⊥ it.filterMapWithPostcondition ---a'-----c'-------⊥

（其中 f a = pure (some a')、f c = pure (some c')，且 f b = f d = d e = pure none。）

终止性质：

• Finite 实例：仅当 it 有限时可用

• Productive 实例：仅当 it 有限时可用

对某些映射函数 f，即使没有提供 Finite（或 Productive）实例，所得迭代器仍会有限（或能产）。例如，若 f 从不返回 none，此组合子便保持能产性；若 f 位于 ExceptT 单子中且总会失败，则即使 it 不有限，it.filterMapWithPostcondition 也会有限。前一种情况下，可以考虑改用开箱即提供更多实例的 map/mapM/mapWithPostcondition 组合子。

在这种情况下，只要 PostconditionT n 单子中携带的后置条件足够强，就能手动证明缺失的实例。若 f 总是返回 some _，合适的后置条件是 fun x => x.isSome；若 f 总会失败，合适的后置条件可以是 fun _ => False。

性能：

基础迭代器 it 每发出一个值，此组合子都会调用 f，并对返回的 Option 值进行模式匹配。

Std.Iter.zip.{w} {α₁ β₁ α₂ β₂ : Type w} [Iterator α₁ Id β₁]
  [Iterator α₂ Id β₂] (left : Iter β₁) (right : Iter β₂) :
  Iter (β₁ × β₂)
Std.Iter.zip.{w} {α₁ β₁ α₂ β₂ : Type w}
  [Iterator α₁ Id β₁] [Iterator α₂ Id β₂]
  (left : Iter β₁) (right : Iter β₂) :
  Iter (β₁ × β₂)

给定两个迭代器 left 和 right，left.zip right 会发出 left 与 right 输出值组成的配对。当其中一个终止时，zip 迭代器也会终止。

弹珠图：

left --a ---b --c right --x --y --⊥ left.zip right -----(a, x)------(b, y)-----⊥

终止性质：

• Finite 实例：仅当 left 或 right 中一个有限、另一个能产时可用

• Productive 实例：仅当 left 与 right 都能产时可用

有时 left.zip right 虽然有限（或能产），上述实例却都不适用。例如，若 left 立即终止而 right 始终跳过，则 left.zip.right 有限，却没有可用的 Finite（甚至 Productive）实例。此类实例需要手动证明。

性能：

left 或 right 每执行一步，此组合子都会引入额外 O(1) 开销。

目前编译器不会拆箱内部状态，因此性能不如理论上所能达到的水平。

Std.Iter.attachWith.{w} {α β : Type w} [Iterator α Id β] (it : Iter β)
  (P : β → Prop)
  (h : ∀ (out : β), it.IsPlausibleIndirectOutput out → P out) :
  Iter { out // P out }
Std.Iter.attachWith.{w} {α β : Type w}
  [Iterator α Id β] (it : Iter β)
  (P : β → Prop)
  (h :
    ∀ (out : β),
      it.IsPlausibleIndirectOutput out →
        P out) :
  Iter { out // P out }

为满足谓词 P 的值组成的迭代器逐个“附加”证明，返回值位于相应子类型 { x // P x } 中的迭代器。

终止性质：

• Finite 实例：仅当基础迭代器有限时可用

• Productive 实例：仅当基础迭代器能产时可用

Std.IterM.toIter.{w} {α β : Type w} (it : IterM Id β) : Iter β
Std.IterM.toIter.{w} {α β : Type w}
  (it : IterM Id β) : Iter β

把 Id 上的单子式迭代器（IterM Id β）转换为纯迭代器（Iter β）。

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

给定迭代器 it 和自然数 n，it.take n 会按顺序输出 it 最前面的至多 n 个值，然后终止。

弹珠图：

it ---a----b---c--d-e--⊥ it.take 3 ---a----b---c⊥ it ---a--⊥ it.take 3 ---a--⊥

终止性质：

• Finite 实例：仅当 it 能产时可用

• Productive 实例：仅当 it 能产时可用

性能：

it 每发出一个值，此组合子都会引入额外 O(1) 开销。

Std.IterM.takeWhile.{w, w'} {α : Type w} {m : Type w → Type w'}
  {β : Type w} [Monad m] (P : β → Bool) (it : IterM m β) : IterM m β
Std.IterM.takeWhile.{w, w'} {α : Type w}
  {m : Type w → Type w'} {β : Type w}
  [Monad m] (P : β → Bool)
  (it : IterM m β) : IterM m β

给定迭代器 it 和谓词 P，it.takeWhile P 会输出 it 发出的值，直到其中一个值被 P 拒绝。若某个发出的值被 P 拒绝，该值会被丢弃，迭代器随即终止。

若 P 是单子式的，请改用 takeWhileM。

弹珠图（忽略单子式效应）：

假设谓词 P 接受 a 和 b，但拒绝 c：

it ---a----b---c--d-e--⊥ it.takeWhile P ---a----b---⊥ it ---a----⊥ it.takeWhile P ---a----⊥

终止性质：

• Finite 实例：仅当 it 有限时可用

• Productive 实例：仅当 it 能产时可用

视 P 而定，即使 it 并非有限（或能产），it.takeWhile P 也可能有限（或能产）。此时需要手动证明 Finite（或 Productive）实例。

性能：

此组合子对 it 的每个输出调用 P，直到谓词求值为假，随后终止。

Std.IterM.takeWhileM.{w, w'} {α : Type w} {m : Type w → Type w'}
  {β : Type w} [Monad m] [MonadAttach m] (P : β → m (ULift Bool))
  (it : IterM m β) : IterM m β
Std.IterM.takeWhileM.{w, w'} {α : Type w}
  {m : Type w → Type w'} {β : Type w}
  [Monad m] [MonadAttach m]
  (P : β → m (ULift Bool))
  (it : IterM m β) : IterM m β

给定迭代器 it 和单子式谓词 P，it.takeWhileM P 会输出 it 发出的值，直到其中一个值被 P 拒绝。若某个发出的值被 P 拒绝，该值会被丢弃，迭代器随即终止。

若 P 是纯谓词，可改用更简单的 takeWhile。

弹珠图（忽略单子式效应）：

假设谓词 P 接受 a 和 b，但拒绝 c：

it ---a----b---c--d-e--⊥ it.takeWhileM P ---a----b---⊥ it ---a----⊥ it.takeWhileM P ---a----⊥

终止性质：

• Finite 实例：仅当 it 有限时可用

• Productive 实例：仅当 it 能产时可用

视 P 而定，即使 it 并非有限（或能产），it.takeWhileM P 也可能有限（或能产）。此时需要手动证明 Finite（或 Productive）实例。

性能：

此组合子对 it 的每个输出调用 P，直到谓词求值为假，随后终止。

Std.IterM.takeWhileWithPostcondition.{w, w'} {α : Type w}
  {m : Type w → Type w'} {β : Type w}
  (P : β → PostconditionT m (ULift Bool)) (it : IterM m β) : IterM m β
Std.IterM.takeWhileWithPostcondition.{w,
    w'}
  {α : Type w} {m : Type w → Type w'}
  {β : Type w}
  (P : β → PostconditionT m (ULift Bool))
  (it : IterM m β) : IterM m β

注意：这是一个非常通用的组合子，需要深入理解单子、依赖类型和终止性证明。变体 takeWhile 与 takeWhileM 更易使用，足以满足大多数用例。

给定迭代器 it 和单子式谓词 P，it.takeWhileWithPostcondition P 会输出 it 发出的值，直到其中一个值被 P 拒绝。若某个发出的值被 P 拒绝，该值会被丢弃，迭代器随即终止。

P 应返回 PostconditionT m (ULift Bool)。PostconditionT 变换器让调用者能在单子 m 中内蕴地证明关于 P 返回值的性质，从而可以依据 P 的具体行为证明终止。

弹珠图（忽略单子式效应）：

假设谓词 P 接受 a 和 b，但拒绝 c：

it ---a----b---c--d-e--⊥ it.takeWhileWithPostcondition P ---a----b---⊥ it ---a----⊥ it.takeWhileWithPostcondition P ---a----⊥

终止性质：

• Finite 实例：仅当 it 有限时可用

• Productive 实例：仅当 it 能产时可用

视 P 而定，即使 it 并非有限（或能产），it.takeWhileWithPostcondition P 也可能有限（或能产）。此时需要手动证明 Finite（或 Productive）实例。

性能：

此组合子对 it 的每个输出调用 P，直到谓词求值为假，随后终止。

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

此组合子只适用于高级用例。

给定有限迭代器 it，返回一个行为与 it 完全相同、但类型与 it.take n 相同的迭代器。

弹珠图：

it ---a----b---c--d-e--⊥ it.toTake ---a----b---c--d-e--⊥

终止性质：

• Finite 实例：总是可用

• Productive 实例：总是可用

性能：

it 每发出一个值，此组合子都会引入额外 O(1) 开销。

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

给定迭代器 it 和自然数 n，it.drop n 会转发 it 除前 n 个之外的所有输出值。

弹珠图：

it ---a----b---c--d-e--⊥ it.drop 3 ---------------d-e--⊥ it ---a--⊥ it.drop 3 ------⊥

终止性质：

• Finite 实例：仅当 it 有限时可用

• Productive 实例：仅当 it 能产时可用

性能：

目前，即使迭代器已不再丢弃任何元素，it 每发出一个值，此组合子仍会引入额外 O(1) 开销。

Std.IterM.dropWhile.{w, w'} {α : Type w} {m : Type w → Type w'}
  {β : Type w} [Monad m] (P : β → Bool) (it : IterM m β) : IterM m β
Std.IterM.dropWhile.{w, w'} {α : Type w}
  {m : Type w → Type w'} {β : Type w}
  [Monad m] (P : β → Bool)
  (it : IterM m β) : IterM m β

给定迭代器 it 和谓词 P，it.dropWhile P 会从第一个被 P 拒绝的值开始，发出 it 所发出的值；此前的元素都被丢弃。

若 P 是单子式的，请改用 dropWhileM。

弹珠图（忽略单子式效应）：

假设谓词 P 接受 a 和 b，但拒绝 c：

it ---a----b---c--d-e--⊥ it.dropWhile P ------------c--d-e--⊥ it ---a----⊥ it.dropWhile P --------⊥

终止性质：

• Finite 实例：仅当 it 有限时可用

• Productive 实例：仅当 it 有限时可用

性能：

此组合子对 it 的每个输出调用 P，直到谓词求值为假。此后，it 每发出一个值，组合子都会引入额外 O(1) 开销。

Std.IterM.dropWhileM.{w, w'} {α : Type w} {m : Type w → Type w'}
  {β : Type w} [Monad m] [MonadAttach m] (P : β → m (ULift Bool))
  (it : IterM m β) : IterM m β
Std.IterM.dropWhileM.{w, w'} {α : Type w}
  {m : Type w → Type w'} {β : Type w}
  [Monad m] [MonadAttach m]
  (P : β → m (ULift Bool))
  (it : IterM m β) : IterM m β

给定迭代器 it 和单子式谓词 P，it.dropWhileM P 会从第一个被 P 拒绝的值开始，发出 it 所发出的值；此前的元素都被丢弃。

若 P 是纯谓词，可改用更简单的 dropWhile。

弹珠图（忽略单子式效应）：

假设谓词 P 接受 a 和 b，但拒绝 c：

it ---a----b---c--d-e--⊥ it.dropWhileM P ------------c--d-e--⊥ it ---a----⊥ it.dropWhileM P --------⊥

终止性质：

• Finite 实例：仅当 it 有限时可用

• Productive 实例：仅当 it 有限时可用

视 P 而定，即使 it 并非有限（或能产），it.dropWhileM P 也可能有限（或能产）。此时需要手动证明 Finite（或 Productive）实例。

性能：

此组合子对 it 的每个输出调用 P，直到谓词求值为假。此后，it 每发出一个值，组合子都会引入额外 O(1) 开销。

Std.IterM.dropWhileWithPostcondition.{w, w'} {α : Type w}
  {m : Type w → Type w'} {β : Type w}
  (P : β → PostconditionT m (ULift Bool)) (it : IterM m β) : IterM m β
Std.IterM.dropWhileWithPostcondition.{w,
    w'}
  {α : Type w} {m : Type w → Type w'}
  {β : Type w}
  (P : β → PostconditionT m (ULift Bool))
  (it : IterM m β) : IterM m β

注意：这是一个非常通用的组合子，需要深入理解单子、依赖类型和终止性证明。变体 dropWhile 与 dropWhileM 更易使用，足以满足大多数用例。

给定迭代器 it 和单子式谓词 P，it.dropWhileWithPostcondition P 会从第一个被 P 拒绝的值开始，发出 it 所发出的值；此前的元素都被丢弃。

P 应返回 PostconditionT m (ULift Bool)。PostconditionT 变换器让调用者能在单子 m 中内蕴地证明关于 P 返回值的性质，从而可以依据 P 的具体行为证明终止。

弹珠图（忽略单子式效应）：

假设谓词 P 接受 a 和 b，但拒绝 c：

it ---a----b---c--d-e--⊥ it.dropWhileWithPostcondition P ------------c--d-e--⊥ it ---a----⊥ it.dropWhileWithPostcondition P --------⊥

终止性质：

• Finite 实例：仅当 it 有限时可用

• Productive 实例：仅当 it 有限时可用

视 P 而定，即使 it 并非有限（或能产），it.dropWhileWithPostcondition P 也可能有限（或能产）。此时需要手动证明 Finite（或 Productive）实例。

性能：

此组合子对 it 的每个输出调用 P，直到谓词求值为假。此后，it 每发出一个值，组合子都会引入额外 O(1) 开销。