From f4ee72b18c4a8a8b0dede6d2bca6a4010074db1d Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Tue, 20 May 2025 16:53:57 +0200
Subject: [PATCH] feat: minimal iterator library (#8358)

This PR introduces a very minimal version of the new iterator library.
It comes with list iterators and various consumers, namely `toArray`,
`toList`, `toListRev`, `ForIn`, `fold`, `foldM` and `drain`. All
consumers also come in a partial variant that can be used without any
proofs. This limited version of the iterator library generates decent
code, even with the old code generator.
---
 src/Std/Data.lean                             |   2 +
 src/Std/Data/Iterators.lean                   | 103 ++++
 src/Std/Data/Iterators/Basic.lean             | 533 ++++++++++++++++++
 src/Std/Data/Iterators/Consumers.lean         |  10 +
 src/Std/Data/Iterators/Consumers/Collect.lean |  57 ++
 src/Std/Data/Iterators/Consumers/Loop.lean    | 104 ++++
 src/Std/Data/Iterators/Consumers/Monadic.lean |   9 +
 .../Iterators/Consumers/Monadic/Collect.lean  | 222 ++++++++
 .../Iterators/Consumers/Monadic/Loop.lean     | 313 ++++++++++
 .../Iterators/Consumers/Monadic/Partial.lean  |  28 +
 src/Std/Data/Iterators/Consumers/Partial.lean |  28 +
 src/Std/Data/Iterators/Internal.lean          |   7 +
 .../Data/Iterators/Internal/Termination.lean  |  59 ++
 src/Std/Data/Iterators/Producers.lean         |   8 +
 src/Std/Data/Iterators/Producers/List.lean    |  22 +
 src/Std/Data/Iterators/Producers/Monadic.lean |   7 +
 .../Iterators/Producers/Monadic/List.lean     |  76 +++
 tests/lean/run/iterators.lean                 |  67 +++
 18 files changed, 1655 insertions(+)
 create mode 100644 src/Std/Data/Iterators.lean
 create mode 100644 src/Std/Data/Iterators/Basic.lean
 create mode 100644 src/Std/Data/Iterators/Consumers.lean
 create mode 100644 src/Std/Data/Iterators/Consumers/Collect.lean
 create mode 100644 src/Std/Data/Iterators/Consumers/Loop.lean
 create mode 100644 src/Std/Data/Iterators/Consumers/Monadic.lean
 create mode 100644 src/Std/Data/Iterators/Consumers/Monadic/Collect.lean
 create mode 100644 src/Std/Data/Iterators/Consumers/Monadic/Loop.lean
 create mode 100644 src/Std/Data/Iterators/Consumers/Monadic/Partial.lean
 create mode 100644 src/Std/Data/Iterators/Consumers/Partial.lean
 create mode 100644 src/Std/Data/Iterators/Internal.lean
 create mode 100644 src/Std/Data/Iterators/Internal/Termination.lean
 create mode 100644 src/Std/Data/Iterators/Producers.lean
 create mode 100644 src/Std/Data/Iterators/Producers/List.lean
 create mode 100644 src/Std/Data/Iterators/Producers/Monadic.lean
 create mode 100644 src/Std/Data/Iterators/Producers/Monadic/List.lean
 create mode 100644 tests/lean/run/iterators.lean

diff --git a/src/Std/Data.lean b/src/Std/Data.lean
index 38b090df67..c28c425c4b 100644
--- a/src/Std/Data.lean
+++ b/src/Std/Data.lean
@@ -23,3 +23,5 @@ import Std.Data.HashSet.RawLemmas
 import Std.Data.DTreeMap.Raw
 import Std.Data.TreeMap.Raw
 import Std.Data.TreeSet.Raw
+
+import Std.Data.Iterators
diff --git a/src/Std/Data/Iterators.lean b/src/Std/Data/Iterators.lean
new file mode 100644
index 0000000000..a5949afa38
--- /dev/null
+++ b/src/Std/Data/Iterators.lean
@@ -0,0 +1,103 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+prelude
+import Std.Data.Iterators.Basic
+import Std.Data.Iterators.Producers
+import Std.Data.Iterators.Consumers
+import Std.Data.Iterators.Internal
+
+/-!
+# Iterators
+
+The `Std.Data.Iterators` module provides a uniform abstraction over data that can be iterated over
+in a sequential way, with a focus on convenience and efficiency. It is heavily inspired by Rust's
+iterator library and Haskell's `streamly`.
+
+An iterator is an abstraction of a sequence of values that may or may not terminate. For example,
+every list can be traversed with an iterator via `List.iter`.
+
+Most users of the iterator API will just put together existing library functions that
+create, combine and consume iterators. Consider a simple example:
+
+```lean
+-- [1, 2, 3].iter : Iter (α := ListIterator α) Nat (α being implicit)
+#check [1, 2, 3].iter
+
+-- 12
+#eval [1, 2, 3].iter.map (· * 2) |>.fold (init := 0) (· + ·)
+```
+
+An iterator that emits values in `β` is an element of the type `Iter (α := ?) β`. The implicit
+type argument `α` contains stateful information about the iterator. `IterM (α := ?) m β` represents
+iterators over a monad `m`. In both cases, the implementation is provided by a typeclass
+`Iterator α m β`, where `m` is a monad in which the iteration happens.
+
+The heart of an iterator `it : Iter β` is its `it.step` function, which returns `it.Step α β`.
+Here, `it.Step` is a type that either (1) provides an output value in `β` and a
+successor iterator (`yield`), (2) provides only a successor iterator with no output (`skip`), or
+(3) signals that the iterator has finished and will provide no more outputs (`done`).
+For technical reasons related to termination proofs, the returned `it.Step` also contains proof
+that it is a "plausible" step obtained from `it`.
+
+The `step` function can also be used by hand:
+
+```lean
+def sumrec (l : List Nat) : Nat :=
+  go (l.iter.map (2 * ·)) 0
+where
+  go it acc :=
+    match it.step with
+    | .yield it' n _ => go it' (acc + n)
+    | .skip it' _ => go it' acc
+    | .done _ => acc
+  termination_by it.finitelyManySteps
+```
+
+In general, iterators do not need to terminate after finitely many steps. This example
+works because the iterator type at hand has an instance of the `Std.Iterators.Finite` typeclass.
+Iterators that may not terminate but will not end up in an infinite sequence of `.skip`
+steps are called productive. This behavior is encoded in the `Std.Iterators.Productive` typeclass.
+
+## Stability
+
+The API for the usage of iterators provided in this module can be considered stable, as well as
+the API for the verification of programms using iterators, unless explicitly stated otherwise.
+
+Contrarily, the API for implementation of new iterators, including the design of the `Iterator`
+typeclass, is still experimental and will change in the future. It is already planned that there
+will be a breaking change to make the iterators more flexible with regard to universes, a change
+that needs to wait for a language feature.
+
+## Module structure
+
+A distinction that cuts through the whole module is that between pure and monadic
+iterators. Each submodule contains a dedicated `Monadic` sub-submodule.
+
+All of the following module names are prefixed with `Std.Data.Iterators`.
+
+### Basic iterator API
+
+* `Basic` defines `Iter` and `IterM` as well as `Iterator`, `Finite`
+  and `Productive` typeclasses.
+* `Producers` provides iterator implementations for common data types.
+* `Consumers` provides functions that take one or more iterators, iterate over them and potentially
+  return some result. Examples are the `toList` function and an instance for the `ForIn` typeclass.
+  These operations allow for what is also known as *internal iteration*, where the caller delegates
+  the control flow during the iteration to the called consumer.
+* `Combinators` will provide operations that transform one or more iterators into a new iterator
+  as soon as the first such combinator has been implemented.
+
+### Verification API
+
+`Lemmas` will provide the means to verify programs that use iterators.
+
+### Implementation details
+
+`Internal` contains code that should not be relied upon because it may change in the future.
+This whole module is explicitly experimental and it is not advisable for downstream users to
+expect stability to implement their own iterators at this point in time.
+
+-/
diff --git a/src/Std/Data/Iterators/Basic.lean b/src/Std/Data/Iterators/Basic.lean
new file mode 100644
index 0000000000..0b589d68f1
--- /dev/null
+++ b/src/Std/Data/Iterators/Basic.lean
@@ -0,0 +1,533 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+prelude
+import Init.Core
+import Init.Classical
+import Init.NotationExtra
+import Init.TacticsExtra
+
+/-!
+### Definition of iterators
+
+This module defines iterators and what it means for an iterator to be finite and productive.
+-/
+
+namespace Std
+
+namespace Iterators
+
+/--
+`BaseIter` is the common data structure underlying `Iter` and `IterM`. API users should never
+use `BaseIter` directly, only `Iter` and `IterM`.
+-/
+structure BaseIter {α : Type w} (m : Type w → Type w') (β : Type w) : Type w where
+  /--
+  Internal implementation detail of the iterator.
+  -/
+  internalState : α
+
+/--
+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 `Std.Data.Iterators.Consumers` for ways to use an iterator. For example, `it.toList` will
+convert a provably finite iterator `it` into a list and `it.allowNontermination.toList` will
+do so even if finiteness cannot be proved. 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:
+
+```lean
+def x : IterM IO Nat := [1, 2, 3].iterM IO
+```
+
+Instead the declaration type needs to be completely omitted:
+
+```lean
+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)
+```
+-/
+def IterM {α : Type w} (m : Type w → Type w') (β : Type w) := BaseIter (α := α) m β
+
+/--
+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 `Std.Data.Iterators.Consumers` for ways to use an iterator. For example, `it.toList` will
+convert a provably finite iterator `it` into a list and `it.allowNontermination.toList` will
+do so even if finiteness cannot be proved. 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:
+
+```lean
+def x : Iter Nat := [1, 2, 3].iter
+```
+
+Instead the declaration type needs to be completely omitted:
+
+```lean
+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)
+```
+-/
+def Iter {α : Type w} (β : Type w) := BaseIter (α := α) Id β
+
+/--
+Converts a pure iterator (`Iter β`) into a monadic iterator (`IterM Id β`) in the
+identity monad `Id`.
+-/
+def Iter.toIterM {α : Type w} {β : Type w} (it : Iter (α := α) β) : IterM (α := α) Id β :=
+  it
+
+/--
+Converts a monadic iterator (`IterM Id β`) over `Id` into a pure iterator (`Iter β`).
+-/
+def IterM.toPureIter {α : Type w} {β : Type w} (it : IterM (α := α) Id β) : Iter (α := α) β :=
+  it
+
+@[simp]
+theorem Iter.toPureIter_toIterM {α : Type w} {β : Type w} (it : Iter (α := α) β) :
+    it.toIterM.toPureIter = it :=
+  rfl
+
+@[simp]
+theorem Iter.toIterM_toPureIter {α : Type w} {β : Type w} (it : IterM (α := α) Id β) :
+    it.toPureIter.toIterM = it :=
+  rfl
+
+section IterStep
+
+variable {α : Type u} {β : Type w}
+
+/--
+`IterStep α β` represents a step taken by an iterator (`Iter β` or `IterM m β`).
+-/
+inductive IterStep (α β) where
+  /--
+  `IterStep.yield it out` describes the situation that an iterator emits `out` and provides `it`
+  as the succeeding iterator.
+  -/
+  | yield : (it : α) → (out : β) → 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.
+  -/
+  | skip : (it : α) → 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.
+  -/
+  | done : IterStep α β
+
+/--
+Returns the succeeding iterator stored in an iterator step or `none` if the step is `.done`
+and the iterator has finished.
+-/
+def IterStep.successor : IterStep α β → Option α
+  | .yield it _ => some it
+  | .skip it => some it
+  | .done => none
+
+/--
+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 PlausibleIterStep (IsPlausibleStep : IterStep α β → Prop) := Subtype IsPlausibleStep
+
+/--
+Match pattern for the `yield` case. See also `IterStep.yield`.
+-/
+@[match_pattern]
+def PlausibleIterStep.yield {IsPlausibleStep : IterStep α β → Prop}
+    (it' : α) (out : β) (h : IsPlausibleStep (.yield it' out)) :
+    PlausibleIterStep IsPlausibleStep :=
+  ⟨.yield it' out, h⟩
+
+/--
+Match pattern for the `skip` case. See also `IterStep.skip`.
+-/
+@[match_pattern]
+def PlausibleIterStep.skip {IsPlausibleStep : IterStep α β → Prop}
+    (it' : α) (h : IsPlausibleStep (.skip it')) : PlausibleIterStep IsPlausibleStep :=
+  ⟨.skip it', h⟩
+
+/--
+Match pattern for the `done` case. See also `IterStep.done`.
+-/
+@[match_pattern]
+def PlausibleIterStep.done {IsPlausibleStep : IterStep α β → Prop}
+    (h : IsPlausibleStep .done) : PlausibleIterStep IsPlausibleStep :=
+  ⟨.done, h⟩
+
+end IterStep
+
+/--
+The typeclass providing 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.
+-/
+class Iterator (α : Type w) (m : Type w → Type w') (β : outParam (Type w)) where
+  IsPlausibleStep : IterM (α := α) m β → IterStep (IterM (α := α) m β) β → Prop
+  step : (it : IterM (α := α) m β) → m (PlausibleIterStep <| IsPlausibleStep it)
+
+section Monadic
+
+/--
+Converts wraps the state of an iterator into an `IterM` object.
+-/
+@[always_inline, inline]
+def toIterM {α : Type w} (it : α) (m : Type w → Type w') (β : Type w) :
+    IterM (α := α) m β :=
+  ⟨it⟩
+
+@[simp]
+theorem toIterM_internalState {α m β} (it : IterM (α := α) m β) :
+    toIterM it.internalState m β = it :=
+  rfl
+
+@[simp]
+theorem internalState_toIterM {α m β} (it : α) :
+    (toIterM it m β).internalState = it :=
+  rfl
+
+/--
+Asserts that certain step is plausibly the successor of a given iterator. What "plausible" means
+is up to the `Iterator` instance but it should be strong enough to allow termination proofs.
+-/
+abbrev IterM.IsPlausibleStep {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] :
+    IterM (α := α) m β → IterStep (IterM (α := α) m β) β → Prop :=
+  Iterator.IsPlausibleStep (α := α) (m := m)
+
+/--
+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.
+-/
+abbrev IterM.Step {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
+    (it : IterM (α := α) m β) :=
+  PlausibleIterStep it.IsPlausibleStep
+
+/--
+Asserts that a certain output value could plausibly be emitted by the given iterator in its next
+step.
+-/
+def IterM.IsPlausibleOutput {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
+    (it : IterM (α := α) m β) (out : β) : Prop :=
+  ∃ it', it.IsPlausibleStep (.yield it' out)
+
+/--
+Asserts that a certain iterator `it'` could plausibly be the directly succeeding iterator of another
+given iterator `it`.
+-/
+def IterM.IsPlausibleSuccessorOf {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
+    (it' it : IterM (α := α) m β) : Prop :=
+  ∃ step, step.successor = some it' ∧ it.IsPlausibleStep step
+
+/--
+Asserts that a certain iterator `it'` could plausibly be the directly succeeding iterator of another
+given iterator `it` while no value is emitted (see `IterStep.skip`).
+-/
+def IterM.IsPlausibleSkipSuccessorOf {α : Type w} {m : Type w → Type w'} {β : Type w}
+    [Iterator α m β] (it' it : IterM (α := α) m β) : Prop :=
+  it.IsPlausibleStep (.skip it')
+
+/--
+Makes a single step with the given iterator `it`, potentially emitting a value and providing a
+succeeding iterator. If this function is used recursively, termination can sometimes be proved with
+the termination measures `it.finitelyManySteps` and `it.finitelyManySkips`.
+-/
+@[always_inline, inline]
+def IterM.step {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
+    (it : IterM (α := α) m β) : m it.Step :=
+  Iterator.step it
+
+end Monadic
+
+section Pure
+
+/--
+Asserts that certain step is plausibly the successor of a given iterator. What "plausible" means
+is up to the `Iterator` instance but it should be strong enough to allow termination proofs.
+-/
+def Iter.IsPlausibleStep {α : Type w} {β : Type w} [Iterator α Id β]
+    (it : Iter (α := α) β) (step : IterStep (Iter (α := α) β) β) : Prop :=
+  it.toIterM.IsPlausibleStep step
+
+/--
+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 Iter.Step {α : Type w} {β : Type w} [Iterator α Id β] (it : Iter (α := α) β) :=
+  PlausibleIterStep (Iter.IsPlausibleStep it)
+
+/--
+Asserts that a certain output value could plausibly be emitted by the given iterator in its next
+step.
+-/
+def Iter.IsPlausibleOutput {α : Type w} {β : Type w} [Iterator α Id β]
+    (it : Iter (α := α) β) (out : β) : Prop :=
+  it.toIterM.IsPlausibleOutput out
+
+/--
+Asserts that a certain iterator `it'` could plausibly be the directly succeeding iterator of another
+given iterator `it`.
+-/
+def Iter.IsPlausibleSuccessorOf {α : Type w} {β : Type w} [Iterator α Id β]
+    (it' it : Iter (α := α) β) : Prop :=
+  it'.toIterM.IsPlausibleSuccessorOf it
+
+/--
+Asserts that a certain iterator `it'` could plausibly be the directly succeeding iterator of another
+given iterator `it` while no value is emitted (see `IterStep.skip`).
+-/
+def Iter.IsPlausibleSkipSuccessorOf {α : Type w} {β : Type w} [Iterator α Id β]
+    (it' it : Iter (α := α) β) : Prop :=
+  it'.toIterM.IsPlausibleSkipSuccessorOf it
+
+/--
+Makes a single step with the given iterator `it`, potentially emitting a value and providing a
+succeeding iterator. If this function is used recursively, termination can sometimes be proved with
+the termination measures `it.finitelyManySteps` and `it.finitelyManySkips`.
+-/
+@[always_inline, inline]
+def Iter.step {α β : Type w} [Iterator α Id β] (it : Iter (α := α) β) : it.Step :=
+  it.toIterM.step
+
+end Pure
+
+section Finite
+
+/--
+`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.
+-/
+class Finite (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β] : Prop where
+  wf : WellFounded (IterM.IsPlausibleSuccessorOf (α := α) (m := m))
+
+/--
+This type is a wrapper around `IterM` so that it becomes a useful termination measure for
+recursion over finite iterators. See also `IterM.finitelyManySteps` and `Iter.finitelyManySteps`.
+-/
+structure IterM.TerminationMeasures.Finite
+    (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β] where
+  it : IterM (α := α) m β
+
+/--
+The relation of plausible successors on `IterM.TerminationMeasures.Finite`. It is well-founded
+if there is a `Finite` instance.
+-/
+def IterM.TerminationMeasures.Finite.Rel
+    {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] :
+    TerminationMeasures.Finite α m → TerminationMeasures.Finite α m → Prop :=
+  Relation.TransGen <| InvImage IterM.IsPlausibleSuccessorOf IterM.TerminationMeasures.Finite.it
+
+instance {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
+    [Finite α m] : WellFoundedRelation (IterM.TerminationMeasures.Finite α m) where
+  rel := IterM.TerminationMeasures.Finite.Rel
+  wf := (InvImage.wf _ Finite.wf).transGen
+
+/--
+Termination measure to be used in well-founded recursive functions recursing over a finite iterator
+(see also `Finite`).
+-/
+def IterM.finitelyManySteps {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
+    [Finite α m] (it : IterM (α := α) m β) : IterM.TerminationMeasures.Finite α m :=
+  ⟨it⟩
+
+/--
+This theorem is used by a `decreasing_trivial` extension. It powers automatic termination proofs
+with `IterM.finitelyManySteps`.
+-/
+theorem IterM.TerminationMeasures.Finite.rel_of_yield
+    {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
+    {it it' : IterM (α := α) m β} {out : β} (h : it.IsPlausibleStep (.yield it' out)) :
+    Rel ⟨it'⟩ ⟨it⟩ := by
+  exact .single ⟨_, rfl, h⟩
+
+@[inherit_doc IterM.TerminationMeasures.Finite.rel_of_yield]
+theorem IterM.TerminationMeasures.Finite.rel_of_skip
+    {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
+    {it it' : IterM (α := α) m β} (h : it.IsPlausibleStep (.skip it')) :
+    Rel ⟨it'⟩ ⟨it⟩ := by
+  exact .single ⟨_, rfl, h⟩
+
+macro_rules | `(tactic| decreasing_trivial) => `(tactic|
+  first
+  | exact IterM.TerminationMeasures.Finite.rel_of_yield ‹_›
+  | exact IterM.TerminationMeasures.Finite.rel_of_skip ‹_›)
+
+@[inherit_doc IterM.finitelyManySteps]
+def Iter.finitelyManySteps {α : Type w} {β : Type w} [Iterator α Id β] [Finite α Id]
+    (it : Iter (α := α) β) : IterM.TerminationMeasures.Finite α Id :=
+  it.toIterM.finitelyManySteps
+
+/--
+This theorem is used by a `decreasing_trivial` extension. It powers automatic termination proofs
+with `IterM.finitelyManySteps`.
+-/
+theorem Iter.TerminationMeasures.Finite.rel_of_yield
+    {α : Type w} {β : Type w} [Iterator α Id β]
+    {it it' : Iter (α := α) β} {out : β} (h : it.IsPlausibleStep (.yield it' out)) :
+    IterM.TerminationMeasures.Finite.Rel ⟨it'⟩ ⟨it⟩ :=
+  IterM.TerminationMeasures.Finite.rel_of_yield h
+
+@[inherit_doc Iter.TerminationMeasures.Finite.rel_of_yield]
+theorem Iter.TerminationMeasures.Finite.rel_of_skip
+    {α : Type w} {β : Type w} [Iterator α Id β]
+    {it it' : Iter (α := α) β} (h : it.IsPlausibleStep (.skip it')) :
+    IterM.TerminationMeasures.Finite.Rel ⟨it'⟩ ⟨it⟩ :=
+  IterM.TerminationMeasures.Finite.rel_of_skip h
+
+macro_rules | `(tactic| decreasing_trivial) => `(tactic|
+  first
+  | exact Iter.TerminationMeasures.Finite.rel_of_yield ‹_›
+  | exact Iter.TerminationMeasures.Finite.rel_of_skip ‹_›)
+
+theorem IterM.isPlausibleSuccessorOf_of_yield
+    {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
+    {it' it : IterM (α := α) m β} {out : β} (h : it.IsPlausibleStep (.yield it' out)) :
+    it'.IsPlausibleSuccessorOf it :=
+  ⟨_, rfl, h⟩
+
+theorem IterM.isPlausibleSuccessorOf_of_skip
+    {α m β} [Iterator α m β] {it it' : IterM (α := α) m β}
+    (h : it.IsPlausibleStep (.skip it')) :
+    it'.IsPlausibleSuccessorOf it :=
+  ⟨_, rfl, h⟩
+
+end Finite
+
+section Productive
+
+/--
+`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.
+-/
+class Productive (α m) {β} [Iterator α m β] : Prop where
+  wf : WellFounded (IterM.IsPlausibleSkipSuccessorOf (α := α) (m := m))
+
+/--
+This type is a wrapper around `IterM` so that it becomes a useful termination measure for
+recursion over productive iterators. See also `IterM.finitelyManySkips` and `Iter.finitelyManySkips`.
+-/
+structure IterM.TerminationMeasures.Productive
+    (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β] where
+  it : IterM (α := α) m β
+
+/--
+The relation of plausible successors while skipping on `IterM.TerminationMeasures.Productive`.
+It is well-founded if there is a `Productive` instance.
+-/
+def IterM.TerminationMeasures.Productive.Rel
+    {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] :
+    TerminationMeasures.Productive α m → TerminationMeasures.Productive α m → Prop :=
+  Relation.TransGen <| InvImage IterM.IsPlausibleSkipSuccessorOf IterM.TerminationMeasures.Productive.it
+
+instance {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
+    [Productive α m] : WellFoundedRelation (IterM.TerminationMeasures.Productive α m) where
+  rel := IterM.TerminationMeasures.Productive.Rel
+  wf := (InvImage.wf _ Productive.wf).transGen
+
+/--
+Termination measure to be used in well-founded recursive functions recursing over a productive
+iterator (see also `Productive`).
+-/
+def IterM.finitelyManySkips {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
+    [Productive α m] (it : IterM (α := α) m β) : IterM.TerminationMeasures.Productive α m :=
+  ⟨it⟩
+
+/--
+This theorem is used by a `decreasing_trivial` extension. It powers automatic termination proofs
+with `IterM.finitelyManySkips`.
+-/
+theorem IterM.TerminationMeasures.Productive.rel_of_skip
+    {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
+    {it it' : IterM (α := α) m β} (h : it.IsPlausibleStep (.skip it')) :
+    Rel ⟨it'⟩ ⟨it⟩ :=
+  .single h
+
+macro_rules | `(tactic| decreasing_trivial) => `(tactic|
+  exact IterM.TerminationMeasures.Productive.rel_of_skip ‹_›)
+
+@[inherit_doc IterM.finitelyManySkips]
+def Iter.finitelyManySkips {α : Type w} {β : Type w} [Iterator α Id β] [Productive α Id]
+    (it : Iter (α := α) β) : IterM.TerminationMeasures.Productive α Id :=
+  it.toIterM.finitelyManySkips
+
+/--
+This theorem is used by a `decreasing_trivial` extension. It powers automatic termination proofs
+with `Iter.finitelyManySkips`.
+-/
+theorem Iter.TerminationMeasures.Productive.rel_of_skip
+    {α : Type w} {β : Type w} [Iterator α Id β]
+    {it it' : Iter (α := α) β} (h : it.IsPlausibleStep (.skip it')) :
+    IterM.TerminationMeasures.Productive.Rel ⟨it'.toIterM⟩ ⟨it.toIterM⟩ :=
+  IterM.TerminationMeasures.Productive.rel_of_skip h
+
+macro_rules | `(tactic| decreasing_trivial) => `(tactic|
+  exact Iter.TerminationMeasures.Productive.rel_of_skip ‹_›)
+
+instance [Iterator α m β] [Finite α m] : Productive α m where
+  wf := by
+    apply Subrelation.wf (r := IterM.IsPlausibleSuccessorOf)
+    · intro it' it h
+      exact IterM.isPlausibleSuccessorOf_of_skip h
+    · exact Finite.wf
+
+end Productive
+
+end Iterators
+
+export Iterators (Iter IterM)
+
+end Std
diff --git a/src/Std/Data/Iterators/Consumers.lean b/src/Std/Data/Iterators/Consumers.lean
new file mode 100644
index 0000000000..6f0e0eae02
--- /dev/null
+++ b/src/Std/Data/Iterators/Consumers.lean
@@ -0,0 +1,10 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+prelude
+import Std.Data.Iterators.Consumers.Monadic
+import Std.Data.Iterators.Consumers.Collect
+import Std.Data.Iterators.Consumers.Loop
+import Std.Data.Iterators.Consumers.Partial
diff --git a/src/Std/Data/Iterators/Consumers/Collect.lean b/src/Std/Data/Iterators/Consumers/Collect.lean
new file mode 100644
index 0000000000..e4104c5625
--- /dev/null
+++ b/src/Std/Data/Iterators/Consumers/Collect.lean
@@ -0,0 +1,57 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+prelude
+import Std.Data.Iterators.Basic
+import Std.Data.Iterators.Consumers.Partial
+import Std.Data.Iterators.Consumers.Monadic.Collect
+
+/-!
+# Collectors
+
+This module provides consumers that collect the values emitted by an iterator in a data structure.
+Concretely, the following operations are provided:
+
+* `Iter.toList`, collecting the values in a list
+* `Iter.toListRev`, collecting the values in a list in reverse order but more efficiently
+* `Iter.toArray`, collecting the values in an array
+
+Some operations are implemented using the `IteratorCollect` and `IteratorCollectPartial`
+typeclasses.
+-/
+
+namespace Std.Iterators
+
+@[always_inline, inline, inherit_doc IterM.toArray]
+def Iter.toArray {α : Type w} {β : Type w}
+    [Iterator α Id β] [Finite α Id] [IteratorCollect α Id] (it : Iter (α := α) β) : Array β :=
+  it.toIterM.toArray
+
+@[always_inline, inline, inherit_doc IterM.Partial.toArray]
+def Iter.Partial.toArray {α : Type w} {β : Type w}
+    [Iterator α Id β] [IteratorCollectPartial α Id] (it : Iter.Partial (α := α) β) : Array β :=
+  it.it.toIterM.allowNontermination.toArray
+
+@[always_inline, inline, inherit_doc IterM.toListRev]
+def Iter.toListRev {α : Type w} {β : Type w}
+    [Iterator α Id β] [Finite α Id] (it : Iter (α := α) β) : List β :=
+  it.toIterM.toListRev
+
+@[always_inline, inline, inherit_doc IterM.Partial.toListRev]
+def Iter.Partial.toListRev {α : Type w} {β : Type w}
+    [Iterator α Id β] (it : Iter.Partial (α := α) β) : List β :=
+  it.it.toIterM.allowNontermination.toListRev
+
+@[always_inline, inline, inherit_doc IterM.toList]
+def Iter.toList {α : Type w} {β : Type w}
+    [Iterator α Id β] [Finite α Id] [IteratorCollect α Id] (it : Iter (α := α) β) : List β :=
+  it.toIterM.toList
+
+@[always_inline, inline, inherit_doc IterM.Partial.toList]
+def Iter.Partial.toList {α : Type w} {β : Type w}
+    [Iterator α Id β] [IteratorCollectPartial α Id] (it : Iter.Partial (α := α) β) : List β :=
+  it.it.toIterM.allowNontermination.toList
+
+end Std.Iterators
diff --git a/src/Std/Data/Iterators/Consumers/Loop.lean b/src/Std/Data/Iterators/Consumers/Loop.lean
new file mode 100644
index 0000000000..c7a0bd2927
--- /dev/null
+++ b/src/Std/Data/Iterators/Consumers/Loop.lean
@@ -0,0 +1,104 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+prelude
+import Std.Data.Iterators.Consumers.Monadic.Loop
+import Std.Data.Iterators.Consumers.Partial
+
+/-!
+# Loop consumers
+
+This module provides consumers that iterate over a given iterator, applying a certain user-supplied
+function in every iteration. Concretely, the following operations are provided:
+
+* `ForIn` instances
+* `Iter.fold`, the analogue of `List.foldl`
+* `Iter.foldM`, the analogue of `List.foldlM`
+
+These operations are implemented using the `IteratorLoop` and `IteratorLoopPartial` typeclasses.
+-/
+
+namespace Std.Iterators
+
+instance (α : Type w) (β : Type w) (n : Type w → Type w') [Monad n]
+    [Iterator α Id β] [Finite α Id] [IteratorLoop α Id n] :
+    ForIn n (Iter (α := α) β) β where
+  forIn it init f :=
+    IteratorLoop.finiteForIn (fun δ (c : Id δ) => pure c.run) |>.forIn it.toIterM init f
+
+instance (α : Type w) (β : Type w) (n : Type w → Type w') [Monad n]
+    [Iterator α Id β] [IteratorLoopPartial α Id n] :
+    ForIn n (Iter.Partial (α := α) β) β where
+  forIn it init f :=
+    letI : MonadLift Id n := ⟨pure⟩
+    ForIn.forIn it.it.toIterM.allowNontermination init f
+
+/--
+Folds a monadic function over an iterator from the left, accumulating a value starting with `init`.
+The accumulated value is combined with the each element of the list in order, using `f`.
+
+It is equivalent to `it.toList.foldlM`.
+
+This function requires a `Finite` instance proving that the iterator will finish after a finite
+number of steps. If the iterator is not finite or such an instance is not available, consider using
+`it.allowNontermination.foldM` instead of `it.foldM`. However, it is not possible to formally
+verify the behavior of the partial variant.
+-/
+@[always_inline, inline]
+def Iter.foldM {n : Type w → Type w} [Monad n]
+    {α : Type w} {β : Type w} {γ : Type w} [Iterator α Id β] [Finite α Id]
+    [IteratorLoop α Id n] (f : γ → β → n γ)
+    (init : γ) (it : Iter (α := α) β) : n γ :=
+  ForIn.forIn it init (fun x acc => ForInStep.yield <$> f acc x)
+
+/--
+Folds a monadic function over an iterator from the left, accumulating a value starting with `init`.
+The accumulated value is combined with the each element of the list in order, using `f`.
+
+It is equivalent to `it.toList.foldlM`.
+
+This is a partial, potentially nonterminating, function. It is not possible to formally verify
+its behavior. If the iterator has a `Finite` instance, consider using `IterM.foldM` instead.
+-/
+@[always_inline, inline]
+def Iter.Partial.foldM {n : Type w → Type w} [Monad n]
+    {α : Type w} {β : Type w} {γ : Type w} [Iterator α Id β]
+    [IteratorLoopPartial α Id n] (f : γ → β → n γ)
+    (init : γ) (it : Iter.Partial (α := α) β) : n γ :=
+  ForIn.forIn it init (fun x acc => ForInStep.yield <$> f acc x)
+
+/--
+Folds a function over an iterator from the left, accumulating a value starting with `init`.
+The accumulated value is combined with the each element of the list in order, using `f`.
+
+It is equivalent to `it.toList.foldl`.
+
+This function requires a `Finite` instance proving that the iterator will finish after a finite
+number of steps. If the iterator is not finite or such an instance is not available, consider using
+`it.allowNontermination.fold` instead of `it.fold`. However, it is not possible to formally
+verify the behavior of the partial variant.
+-/
+@[always_inline, inline]
+def Iter.fold {α : Type w} {β : Type w} {γ : Type w} [Iterator α Id β] [Finite α Id]
+    [IteratorLoop α Id Id] (f : γ → β → γ)
+    (init : γ) (it : Iter (α := α) β) : γ :=
+  ForIn.forIn (m := Id) it init (fun x acc => ForInStep.yield (f acc x))
+
+/--
+Folds a function over an iterator from the left, accumulating a value starting with `init`.
+The accumulated value is combined with the each element of the list in order, using `f`.
+
+It is equivalent to `it.toList.foldl`.
+
+This is a partial, potentially nonterminating, function. It is not possible to formally verify
+its behavior. If the iterator has a `Finite` instance, consider using `IterM.fold` instead.
+-/
+@[always_inline, inline]
+def Iter.Partial.fold {α : Type w} {β : Type w} {γ : Type w} [Iterator α Id β]
+    [IteratorLoopPartial α Id Id] (f : γ → β → γ)
+    (init : γ) (it : Iter.Partial (α := α) β) : γ :=
+  ForIn.forIn (m := Id) it init (fun x acc => ForInStep.yield (f acc x))
+
+end Std.Iterators
diff --git a/src/Std/Data/Iterators/Consumers/Monadic.lean b/src/Std/Data/Iterators/Consumers/Monadic.lean
new file mode 100644
index 0000000000..6e861afb81
--- /dev/null
+++ b/src/Std/Data/Iterators/Consumers/Monadic.lean
@@ -0,0 +1,9 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+prelude
+import Std.Data.Iterators.Consumers.Monadic.Collect
+import Std.Data.Iterators.Consumers.Monadic.Loop
+import Std.Data.Iterators.Consumers.Monadic.Partial
diff --git a/src/Std/Data/Iterators/Consumers/Monadic/Collect.lean b/src/Std/Data/Iterators/Consumers/Monadic/Collect.lean
new file mode 100644
index 0000000000..dda29047c6
--- /dev/null
+++ b/src/Std/Data/Iterators/Consumers/Monadic/Collect.lean
@@ -0,0 +1,222 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+prelude
+import Std.Data.Iterators.Consumers.Monadic.Partial
+
+/-!
+# Collectors
+
+This module provides consumers that collect the values emitted by an iterator in a data structure.
+Concretely, the following operations are provided:
+
+* `IterM.toList`, collecting the values in a list
+* `IterM.toListRev`, collecting the values in a list in reverse order but more efficiently
+* `IterM.toArray`, collecting the values in an array
+
+Some producers and combinators provide specialized implementations. These are captured by the
+`IteratorCollect` and `IteratorCollectPartial` typeclasses. They should be implemented by all
+types of iterators. A default implementation is provided. The typeclass `LawfulIteratorCollect`
+asserts that an `IteratorCollect` instance equals the default implementation.
+-/
+
+namespace Std.Iterators
+
+section Typeclasses
+
+/--
+`IteratorCollect α m` provides efficient implementations of collectors for `α`-based
+iterators. Right now, it is limited to a potentially optimized `toArray` implementation.
+
+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.
+-/
+class IteratorCollect (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β] where
+  toArrayMapped [Finite α m] : ∀ {γ : Type w}, (β → m γ) → IterM (α := α) m β → m (Array γ)
+
+/--
+`IteratorCollectPartial α m` provides efficient implementations of collectors for `α`-based
+iterators. Right now, it is limited to a potentially optimized partial `toArray` implementation.
+
+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.
+-/
+class IteratorCollectPartial
+  (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β] where
+    toArrayMappedPartial : ∀ {γ : Type w}, (β → m γ) → IterM (α := α) m β → m (Array γ)
+
+end Typeclasses
+
+section ToArray
+
+/--
+This is an internal function used in `IteratorCollect.defaultImplementation`.
+
+It iterates over an iterator and applies `f` whenever a value is emitted before inserting the result
+of `f` into an array.
+-/
+@[always_inline, inline]
+def IterM.DefaultConsumers.toArrayMapped {α : Type w} {m : Type w → Type w'} [Monad m] {β : Type w}
+    [Iterator α m β] [Finite α m] {γ : Type w} (f : β → m γ) (it : IterM (α := α) m β) : m (Array γ) :=
+  go it #[]
+where
+  @[specialize]
+  go [Monad m] [Finite α m] (it : IterM (α := α) m β) a := do
+    match ← it.step with
+    | .yield it' b _ => go it' (a.push (← f b))
+    | .skip it' _ => go it' a
+    | .done _ => return a
+  termination_by it.finitelyManySteps
+
+/--
+This is the default implementation of the `IteratorLoop` class.
+It simply iterates through the iterator using `IterM.step`, incrementally building up the desired
+data structure. For certain iterators, more efficient implementations are possible and should be
+used instead.
+-/
+@[always_inline, inline]
+def IteratorCollect.defaultImplementation {α : Type w} {m : Type w → Type w'}
+    [Monad m] [Iterator α m β] : IteratorCollect α m where
+  toArrayMapped := IterM.DefaultConsumers.toArrayMapped
+
+/--
+Asserts that a given `IteratorCollect` instance is equal to `IteratorCollect.defaultImplementation`.
+(Even though equal, the given instance might be vastly more efficient.)
+-/
+class LawfulIteratorCollect (α : Type w) (m : Type w → Type w') [Monad m] [Iterator α m β]
+    [i : IteratorCollect α m] where
+  lawful : i = .defaultImplementation
+
+instance (α : Type w) (m : Type w → Type w') [Monad m] [Iterator α m β]
+    [Monad m] [Iterator α m β] [Finite α m] :
+    haveI : IteratorCollect α m := .defaultImplementation
+    LawfulIteratorCollect α m :=
+  letI : IteratorCollect α m := .defaultImplementation
+  ⟨rfl⟩
+
+/--
+This is an internal function used in `IteratorCollectPartial.defaultImplementation`.
+
+It iterates over an iterator and applies `f` whenever a value is emitted before inserting the result
+of `f` into an array.
+-/
+@[always_inline, inline]
+partial def IterM.DefaultConsumers.toArrayMappedPartial {α : Type w} {m : Type w → Type w'} [Monad m] {β : Type w}
+    [Iterator α m β] {γ : Type w} (f : β → m γ) (it : IterM (α := α) m β) : m (Array γ) :=
+  go it #[]
+where
+  @[specialize]
+  go [Monad m] (it : IterM (α := α) m β) a := do
+    match ← it.step with
+    | .yield it' b _ => go it' (a.push (← f b))
+    | .skip it' _ => go it' a
+    | .done _ => return a
+
+/--
+This is the default implementation of the `IteratorLoopPartial` class.
+It simply iterates through the iterator using `IterM.step`, incrementally building up the desired
+data structure. For certain iterators, more efficient implementations are possible and should be
+used instead.
+-/
+@[always_inline, inline]
+def IteratorCollectPartial.defaultImplementation {α : Type w} {m : Type w → Type w'}
+    [Monad m] [Iterator α m β] : IteratorCollectPartial α m where
+  toArrayMappedPartial := IterM.DefaultConsumers.toArrayMappedPartial
+
+/--
+Traverses the given iterator and stores the emitted values in an array.
+
+This function requires a `Finite` instance proving that the iterator will finish after a finite
+number of steps. If the iterator is not finite or such an instance is not available, consider using
+`it.allowNontermination.toArray` instead of `it.toArray`. However, it is not possible to formally
+verify the behavior of the partial variant.
+-/
+@[always_inline, inline]
+def IterM.toArray {α : Type w} {m : Type w → Type w'} {β : Type w} [Monad m]
+    [Iterator α m β] [Finite α m] [IteratorCollect α m] (it : IterM (α := α) m β) : m (Array β) :=
+  IteratorCollect.toArrayMapped pure it
+
+/--
+Traverses the given iterator and stores the emitted values in an array.
+
+This is a partial, potentially nonterminating, function. It is not possible to formally verify
+its behavior. If the iterator has a `Finite` instance, consider using `IterM.toArray` instead.
+-/
+@[always_inline, inline]
+def IterM.Partial.toArray {α : Type w} {m : Type w → Type w'} {β : Type w} [Monad m]
+    [Iterator α m β] (it : IterM.Partial (α := α) m β) [IteratorCollectPartial α m] : m (Array β) :=
+  IteratorCollectPartial.toArrayMappedPartial pure it.it
+
+end ToArray
+
+/--
+Traverses the given iterator and stores the emitted values in reverse order in a list. Because
+lists are prepend-only, this `toListRev` is usually more efficient that `toList`.
+
+This function requires a `Finite` instance proving that the iterator will finish after a finite
+number of steps. If the iterator is not finite or such an instance is not available, consider using
+`it.allowNontermination.toListRev` instead of `it.toListRev`. However, it is not possible to
+formally verify the behavior of the partial variant.
+-/
+@[inline]
+def IterM.toListRev {α : Type w} {m : Type w → Type w'} [Monad m] {β : Type w}
+    [Iterator α m β] [Finite α m] (it : IterM (α := α) m β) : m (List β) :=
+  go it []
+where
+  go [Finite α m] it bs := do
+    match ← it.step with
+    | .yield it' b _ => go it' (b :: bs)
+    | .skip it' _ => go it' bs
+    | .done _ => return bs
+  termination_by it.finitelyManySteps
+
+/--
+Traverses the given iterator and stores the emitted values in reverse order in a list. Because
+lists are prepend-only, this `toListRev` is usually more efficient that `toList`.
+
+This is a partial, potentially nonterminating, function. It is not possible to formally verify
+its behavior. If the iterator has a `Finite` instance, consider using `IterM.toListRev` instead.
+-/
+@[always_inline, inline]
+partial def IterM.Partial.toListRev {α : Type w} {m : Type w → Type w'} [Monad m] {β : Type w}
+    [Iterator α m β] (it : IterM.Partial (α := α) m β) : m (List β) :=
+  go it.it []
+where
+  @[specialize]
+  go it bs := do
+    match ← it.step with
+    | .yield it' b _ => go it' (b :: bs)
+    | .skip it' _ => go it' bs
+    | .done _ => return bs
+
+/--
+Traverses the given iterator and stores the emitted values in a list. Because
+lists are prepend-only, `toListRev` is usually more efficient that `toList`.
+
+This function requires a `Finite` instance proving that the iterator will finish after a finite
+number of steps. If the iterator is not finite or such an instance is not available, consider using
+`it.allowNontermination.toList` instead of `it.toList`. However, it is not possible to
+formally verify the behavior of the partial variant.
+-/
+@[always_inline, inline]
+def IterM.toList {α : Type w} {m : Type w → Type w'} [Monad m] {β : Type w}
+    [Iterator α m β] [Finite α m] [IteratorCollect α m] (it : IterM (α := α) m β) : m (List β) :=
+  Array.toList <$> IterM.toArray it
+
+/--
+Traverses the given iterator and stores the emitted values in a list. Because
+lists are prepend-only, `toListRev` is usually more efficient that `toList`.
+
+This is a partial, potentially nonterminating, function. It is not possible to formally verify
+its behavior. If the iterator has a `Finite` instance, consider using `IterM.toList` instead.
+-/
+@[always_inline, inline]
+def IterM.Partial.toList {α : Type w} {m : Type w → Type w'} [Monad m] {β : Type w}
+    [Iterator α m β] (it : IterM.Partial (α := α) m β) [IteratorCollectPartial α m] : m (List β) :=
+  Array.toList <$> it.toArray
+
+end Std.Iterators
diff --git a/src/Std/Data/Iterators/Consumers/Monadic/Loop.lean b/src/Std/Data/Iterators/Consumers/Monadic/Loop.lean
new file mode 100644
index 0000000000..4eadc20bc0
--- /dev/null
+++ b/src/Std/Data/Iterators/Consumers/Monadic/Loop.lean
@@ -0,0 +1,313 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+prelude
+import Init.RCases
+import Std.Data.Iterators.Basic
+import Std.Data.Iterators.Consumers.Monadic.Partial
+
+/-!
+# Loop-based consumers
+
+This module provides consumers that iterate over a given iterator, applying a certain user-supplied
+function in every iteration. Concretely, the following operations are provided:
+
+* `ForIn` instances
+* `IterM.fold`, the analogue of `List.foldl`
+* `IterM.foldM`, the analogue of `List.foldlM`
+* `IterM.drain`, which iterates over the whole iterator and discards all emitted values. It can
+  be used to apply the monadic effects of the iterator.
+
+Some producers and combinators provide specialized implementations. These are captured by the
+`IteratorLoop` and `IteratorLoopPartial` typeclasses. They should be implemented by all
+types of iterators. A default implementation is provided. The typeclass `LawfulIteratorLoop`
+asserts that an `IteratorLoop` instance equals the default implementation.
+-/
+
+namespace Std.Iterators
+
+section Typeclasses
+
+/--
+Relation that needs to be well-formed in order for a loop over an iterator to terminate.
+It is assumed that the `plausible_forInStep` predicate relates the input and output of the
+stepper function.
+-/
+def IteratorLoop.rel (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β]
+    {γ : Type x} (plausible_forInStep : β → γ → ForInStep γ → Prop)
+    (p' p : IterM (α := α) m β × γ) : Prop :=
+  (∃ b, p.1.IsPlausibleStep (.yield p'.1 b) ∧ plausible_forInStep b p.2 (.yield p'.2)) ∨
+    (p.1.IsPlausibleStep (.skip p'.1) ∧ p'.2 = p.2)
+
+/--
+Asserts that `IteratorLoop.rel` is well-founded.
+-/
+def IteratorLoop.WellFounded (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β]
+    {γ : Type x} (plausible_forInStep : β → γ → ForInStep γ → Prop) : Prop :=
+    _root_.WellFounded (IteratorLoop.rel α m plausible_forInStep)
+
+/--
+`IteratorLoop α m` provides efficient implementations of loop-based consumers for `α`-based
+iterators. The basis is a `ForIn`-style loop construct with the complication that it can be used
+for infinite iterators, too -- given a proof that the given loop will nevertheless terminate.
+
+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.
+-/
+class IteratorLoop (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β]
+    (n : Type w → Type w'') where
+  forIn : ∀ (_lift : (γ : Type w) → m γ → n γ) (γ : Type w),
+      (plausible_forInStep : β → γ → ForInStep γ → Prop) →
+      IteratorLoop.WellFounded α m plausible_forInStep →
+      IterM (α := α) m β → γ →
+      ((b : β) → (c : γ) → n (Subtype (plausible_forInStep b c))) → n γ
+
+/--
+`IteratorLoopPartial α m` provides efficient implementations of loop-based consumers for `α`-based
+iterators. The basis is a partial, i.e. potentially nonterminating, `ForIn` instance.
+
+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.
+-/
+class IteratorLoopPartial (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β]
+    (n : Type w → Type w'') where
+  forInPartial : ∀ (_lift : (γ : Type w) → m γ → n γ) {γ : Type w},
+      IterM (α := α) m β → γ → ((b : β) → (c : γ) → n (ForInStep γ)) → n γ
+
+end Typeclasses
+
+private def IteratorLoop.WFRel {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
+    {γ : Type x} {plausible_forInStep : β → γ → ForInStep γ → Prop}
+    (_wf : WellFounded α m plausible_forInStep) :=
+  IterM (α := α) m β × γ
+
+private def IteratorLoop.WFRel.mk {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
+    {γ : Type x} {plausible_forInStep : β → γ → ForInStep γ → Prop}
+    (wf : WellFounded α m plausible_forInStep) (it : IterM (α := α) m β) (c : γ) :
+    IteratorLoop.WFRel wf :=
+  (it, c)
+
+instance {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
+    {γ : Type x} {plausible_forInStep : β → γ → ForInStep γ → Prop}
+    (wf : IteratorLoop.WellFounded α m plausible_forInStep) :
+    WellFoundedRelation (IteratorLoop.WFRel wf) where
+  rel := IteratorLoop.rel α m plausible_forInStep
+  wf := wf
+
+/--
+This is the loop implementation of the default instance `IteratorLoop.defaultImplementation`.
+-/
+@[specialize]
+def IterM.DefaultConsumers.forIn {m : Type w → Type w'} {α : Type w} {β : Type w}
+    [Iterator α m β]
+    {n : Type w → Type w''} [Monad n]
+    (lift : ∀ γ, m γ → n γ) (γ : Type w)
+    (plausible_forInStep : β → γ → ForInStep γ → Prop)
+    (wf : IteratorLoop.WellFounded α m plausible_forInStep)
+    (it : IterM (α := α) m β) (init : γ)
+    (f : (b : β) → (c : γ) → n (Subtype (plausible_forInStep b c))) : n γ :=
+  haveI : WellFounded _ := wf
+  letI : MonadLift m n := ⟨fun {γ} => lift γ⟩
+  do
+    match ← it.step with
+    | .yield it' out _ =>
+      match ← f out init with
+      | ⟨.yield c, _⟩ => IterM.DefaultConsumers.forIn lift _ plausible_forInStep wf it' c f
+      | ⟨.done c, _⟩ => return c
+    | .skip it' _ => IterM.DefaultConsumers.forIn lift _ plausible_forInStep wf it' init f
+    | .done _ => return init
+termination_by IteratorLoop.WFRel.mk wf it init
+decreasing_by
+  · exact Or.inl ⟨out, ‹_›, ‹_›⟩
+  · exact Or.inr ⟨‹_›, rfl⟩
+
+/--
+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.
+-/
+@[always_inline, inline]
+def IteratorLoop.defaultImplementation {α : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
+    [Monad n] [Iterator α m β] :
+    IteratorLoop α m n where
+  forIn lift := IterM.DefaultConsumers.forIn lift
+
+/--
+Asserts that a given `IteratorLoop` instance is equal to `IteratorLoop.defaultImplementation`.
+(Even though equal, the given instance might be vastly more efficient.)
+-/
+class LawfulIteratorLoop (α : Type w) (m : Type w → Type w') (n : Type w → Type w'')
+    [Monad n] [Iterator α m β] [Finite α m] [i : IteratorLoop α m n] where
+  lawful : i = .defaultImplementation
+
+/--
+This is the loop implementation of the default instance `IteratorLoopPartial.defaultImplementation`.
+-/
+@[specialize]
+partial def IterM.DefaultConsumers.forInPartial {m : Type w → Type w'} {α : Type w} {β : Type w}
+    [Iterator α m β]
+    {n : Type w → Type w''} [Monad n]
+    (lift : ∀ γ, m γ → n γ) (γ : Type w)
+    (it : IterM (α := α) m β) (init : γ)
+    (f : (b : β) → (c : γ) → n (ForInStep γ)) : n γ :=
+  letI : MonadLift m n := ⟨fun {γ} => lift γ⟩
+  do
+    match ← it.step with
+    | .yield it' out _ =>
+      match ← f out init with
+      | .yield c => IterM.DefaultConsumers.forInPartial lift _ it' c f
+      | .done c => return c
+    | .skip it' _ => IterM.DefaultConsumers.forInPartial lift _ it' init f
+    | .done _ => return init
+
+/--
+This is the default implementation of the `IteratorLoopPartial` class.
+It simply iterates through the iterator using `IterM.step`. For certain iterators, more efficient
+implementations are possible and should be used instead.
+-/
+@[always_inline, inline]
+def IteratorLoopPartial.defaultImplementation {α : Type w} {m : Type w → Type w'} {n : Type w → Type w'}
+    [Monad m] [Monad n] [Iterator α m β] :
+    IteratorLoopPartial α m n where
+  forInPartial lift := IterM.DefaultConsumers.forInPartial lift _
+
+instance (α : Type w) (m : Type w → Type w') (n : Type w → Type w')
+    [Monad m] [Monad n] [Iterator α m β] [Finite α m] :
+    letI : IteratorLoop α m n := .defaultImplementation
+    LawfulIteratorLoop α m n :=
+  letI : IteratorLoop α m n := .defaultImplementation
+  ⟨rfl⟩
+
+/--
+This `ForIn`-style loop construct traverses a finite iterator using an `IteratorLoop` instance.
+-/
+@[always_inline, inline]
+def IteratorLoop.finiteForIn {m : Type w → Type w'} {n : Type w → Type w''}
+    {α : Type w} {β : Type w} [Iterator α m β] [Finite α m] [IteratorLoop α m n]
+    (lift : ∀ γ, m γ → n γ) :
+    ForIn n (IterM (α := α) m β) β where
+  forIn {γ} [Monad n] it init f :=
+    IteratorLoop.forIn (α := α) (m := m) lift γ (fun _ _ _ => True)
+      (by
+        apply Subrelation.wf
+          (r := InvImage IterM.TerminationMeasures.Finite.Rel (fun p => p.1.finitelyManySteps))
+        · intro p' p h
+          apply Relation.TransGen.single
+          obtain ⟨b, h, _⟩ | ⟨h, _⟩ := h
+          · exact ⟨.yield p'.fst b, rfl, h⟩
+          · exact ⟨.skip p'.fst, rfl, h⟩
+        · apply InvImage.wf
+          exact WellFoundedRelation.wf)
+      it init ((⟨·, .intro⟩) <$> f · ·)
+
+instance {m : Type w → Type w'} {n : Type w → Type w''}
+    {α : Type w} {β : Type w} [Iterator α m β] [Finite α m] [IteratorLoop α m n]
+    [MonadLiftT m n] :
+    ForIn n (IterM (α := α) m β) β := IteratorLoop.finiteForIn (fun _ => monadLift)
+
+instance {m : Type w → Type w'} {n : Type w → Type w''}
+    {α : Type w} {β : Type w} [Iterator α m β] [IteratorLoopPartial α m n] [MonadLiftT m n] :
+    ForIn n (IterM.Partial (α := α) m β) β where
+  forIn it init f := IteratorLoopPartial.forInPartial (α := α) (m := m) (fun _ => monadLift) it.it init f
+
+/--
+Folds a monadic function over an iterator from the left, accumulating a value starting with `init`.
+The accumulated value is combined with the each element of the list in order, using `f`.
+
+The monadic effects of `f` are interleaved with potential effects caused by the iterator's step
+function. Therefore, it may *not* be equivalent to `(← it.toList).foldlM`.
+
+This function requires a `Finite` instance proving that the iterator will finish after a finite
+number of steps. If the iterator is not finite or such an instance is not available, consider using
+`it.allowNontermination.foldM` instead of `it.foldM`. However, it is not possible to formally
+verify the behavior of the partial variant.
+-/
+@[always_inline, inline]
+def IterM.foldM {m : Type w → Type w'} {n : Type w → Type w'} [Monad n]
+    {α : Type w} {β : Type w} {γ : Type w} [Iterator α m β] [Finite α m] [IteratorLoop α m n]
+    [MonadLiftT m n]
+    (f : γ → β → n γ) (init : γ) (it : IterM (α := α) m β) : n γ :=
+  ForIn.forIn it init (fun x acc => ForInStep.yield <$> f acc x)
+
+/--
+Folds a monadic function over an iterator from the left, accumulating a value starting with `init`.
+The accumulated value is combined with the each element of the list in order, using `f`.
+
+The monadic effects of `f` are interleaved with potential effects caused by the iterator's step
+function. Therefore, it may *not* be equivalent to `it.toList.foldlM`.
+
+This is a partial, potentially nonterminating, function. It is not possible to formally verify
+its behavior. If the iterator has a `Finite` instance, consider using `IterM.foldM` instead.
+-/
+@[always_inline, inline]
+def IterM.Partial.foldM {m : Type w → Type w'} {n : Type w → Type w'} [Monad n]
+    {α : Type w} {β : Type w} {γ : Type w} [Iterator α m β] [IteratorLoopPartial α m n]
+    [MonadLiftT m n]
+    (f : γ → β → n γ) (init : γ) (it : IterM.Partial (α := α) m β) : n γ :=
+  ForIn.forIn it init (fun x acc => ForInStep.yield <$> f acc x)
+
+/--
+Folds a function over an iterator from the left, accumulating a value starting with `init`.
+The accumulated value is combined with the each element of the list in order, using `f`.
+
+It is equivalent to `it.toList.foldl`.
+
+This function requires a `Finite` instance proving that the iterator will finish after a finite
+number of steps. If the iterator is not finite or such an instance is not available, consider using
+`it.allowNontermination.fold` instead of `it.fold`. However, it is not possible to formally
+verify the behavior of the partial variant.
+-/
+@[always_inline, inline]
+def IterM.fold {m : Type w → Type w'} {α : Type w} {β : Type w} {γ : Type w} [Monad m]
+    [Iterator α m β] [Finite α m] [IteratorLoop α m m]
+    (f : γ → β → γ) (init : γ) (it : IterM (α := α) m β) : m γ :=
+  ForIn.forIn (m := m) it init (fun x acc => pure (ForInStep.yield (f acc x)))
+
+/--
+Folds a function over an iterator from the left, accumulating a value starting with `init`.
+The accumulated value is combined with the each element of the list in order, using `f`.
+
+It is equivalent to `it.toList.foldl`.
+
+This is a partial, potentially nonterminating, function. It is not possible to formally verify
+its behavior. If the iterator has a `Finite` instance, consider using `IterM.fold` instead.
+-/
+@[always_inline, inline]
+def IterM.Partial.fold {m : Type w → Type w'} {α : Type w} {β : Type w} {γ : Type w}
+    [Monad m] [Iterator α m β] [IteratorLoopPartial α m m]
+    (f : γ → β → γ) (init : γ) (it : IterM.Partial (α := α) m β) : m γ :=
+  ForIn.forIn (m := m) it init (fun x acc => pure (ForInStep.yield (f acc x)))
+
+/--
+Iterates over the whole iterator, applying the monadic effects of each step, discarding all
+emitted values.
+
+This function requires a `Finite` instance proving that the iterator will finish after a finite
+number of steps. If the iterator is not finite or such an instance is not available, consider using
+`it.allowNontermination.drain` instead of `it.drain`. However, it is not possible to formally
+verify the behavior of the partial variant.
+-/
+@[always_inline, inline]
+def IterM.drain {α : Type w} {m : Type w → Type w'} [Monad m] {β : Type w}
+    [Iterator α m β] [Finite α m] (it : IterM (α := α) m β) [IteratorLoop α m m] :
+    m PUnit :=
+  it.foldM (γ := PUnit) (fun _ _ => pure .unit) .unit
+
+/--
+Iterates over the whole iterator, applying the monadic effects of each step, discarding all
+emitted values.
+
+This is a partial, potentially nonterminating, function. It is not possible to formally verify
+its behavior. If the iterator has a `Finite` instance, consider using `IterM.drain` instead.
+-/
+@[always_inline, inline]
+def IterM.Partial.drain {α : Type w} {m : Type w → Type w'} [Monad m] {β : Type w}
+    [Iterator α m β] (it : IterM.Partial (α := α) m β) [IteratorLoopPartial α m m] :
+    m PUnit :=
+  it.foldM (γ := PUnit) (fun _ _ => pure .unit) .unit
+
+end Std.Iterators
diff --git a/src/Std/Data/Iterators/Consumers/Monadic/Partial.lean b/src/Std/Data/Iterators/Consumers/Monadic/Partial.lean
new file mode 100644
index 0000000000..0729615bdc
--- /dev/null
+++ b/src/Std/Data/Iterators/Consumers/Monadic/Partial.lean
@@ -0,0 +1,28 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+prelude
+import Std.Data.Iterators.Basic
+
+namespace Std.Iterators
+
+/--
+A wrapper around an iterator that provides partial consumers. See `IterM.allowNontermination`.
+-/
+structure IterM.Partial {α : Type w} (m : Type w → Type w') (β : Type w) where
+  it : IterM (α := α) m β
+
+/--
+For an iterator `it`, `it.allowNontermination` provides potentially nonterminating variants of
+consumers such as `toList`. They can be used without any proof of termination such as `Finite`
+or `Productive`, but as they are implemented with the `partial` declaration modifier, they are
+opaque for the kernel and it is impossible to prove anything about them.
+-/
+@[always_inline, inline]
+def IterM.allowNontermination {α : Type w} {m : Type w → Type w'} {β : Type w}
+    (it : IterM (α := α) m β) : IterM.Partial (α := α) m β :=
+  ⟨it⟩
+
+end Std.Iterators
diff --git a/src/Std/Data/Iterators/Consumers/Partial.lean b/src/Std/Data/Iterators/Consumers/Partial.lean
new file mode 100644
index 0000000000..2d16d5b93a
--- /dev/null
+++ b/src/Std/Data/Iterators/Consumers/Partial.lean
@@ -0,0 +1,28 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+prelude
+import Std.Data.Iterators.Basic
+
+namespace Std.Iterators
+
+/--
+A wrapper around an iterator that provides partial consumers. See `Iter.allowNontermination`.
+-/
+structure Iter.Partial {α : Type w} (β : Type w) where
+  it : Iter (α := α) β
+
+/--
+For an iterator `it`, `it.allowNontermination` provides potentially nonterminating variants of
+consumers such as `toList`. They can be used without any proof of termination such as `Finite`
+or `Productive`, but as they are implemented with the `partial` declaration modifier, they are
+opaque for the kernel and it is impossible to prove anything about them.
+-/
+@[always_inline, inline]
+def Iter.allowNontermination {α : Type w} {β : Type w}
+    (it : Iter (α := α) β) : Iter.Partial (α := α) β :=
+  ⟨it⟩
+
+end Std.Iterators
diff --git a/src/Std/Data/Iterators/Internal.lean b/src/Std/Data/Iterators/Internal.lean
new file mode 100644
index 0000000000..aa5ab7f1cd
--- /dev/null
+++ b/src/Std/Data/Iterators/Internal.lean
@@ -0,0 +1,7 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+prelude
+import Std.Data.Iterators.Internal.Termination
diff --git a/src/Std/Data/Iterators/Internal/Termination.lean b/src/Std/Data/Iterators/Internal/Termination.lean
new file mode 100644
index 0000000000..7da422b1d0
--- /dev/null
+++ b/src/Std/Data/Iterators/Internal/Termination.lean
@@ -0,0 +1,59 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+prelude
+import Std.Data.Iterators.Basic
+
+/-!
+This is an internal module used by iterator implementations.
+-/
+
+namespace Std.Iterators
+
+/--
+Internal implementation detail of the iterator library.
+The purpose of this class is that it implies a `Finite` instance but
+it is more convenient to implement.
+-/
+structure FinitenessRelation (α : Type w) (m : Type w → Type w') {β : Type w}
+    [Iterator α m β] where
+  rel : (IterM (α := α) m β) → (IterM (α := α) m β) → Prop
+  wf : WellFounded rel
+  subrelation : ∀ {it it'}, it'.IsPlausibleSuccessorOf it → rel it' it
+
+theorem Finite.of_finitenessRelation
+    {α : Type w} {m : Type w → Type w'} {β : Type w}
+    [Iterator α m β] (r : FinitenessRelation α m) : Finite α m where
+  wf := by
+    refine Subrelation.wf (r := r.rel) ?_ ?_
+    · intro x y h
+      apply FinitenessRelation.subrelation
+      exact h
+    · apply InvImage.wf
+      exact r.wf
+
+/--
+Internal implementation detail of the iterator library.
+The purpose of this class is that it implies a `Productive` instance but
+it is more convenient to implement.
+-/
+structure ProductivenessRelation (α : Type w) (m : Type w → Type w') {β : Type w}
+    [Iterator α m β] where
+  rel : (IterM (α := α) m β) → (IterM (α := α) m β) → Prop
+  wf : WellFounded rel
+  subrelation : ∀ {it it'}, it'.IsPlausibleSkipSuccessorOf it → rel it' it
+
+theorem Productive.of_productivenessRelation
+    {α : Type w} {m : Type w → Type w'} {β : Type w}
+    [Iterator α m β] (r : ProductivenessRelation α m) : Productive α m where
+  wf := by
+    refine Subrelation.wf (r := r.rel) ?_ ?_
+    · intro x y h
+      apply ProductivenessRelation.subrelation
+      exact h
+    · apply InvImage.wf
+      exact r.wf
+
+end Std.Iterators
diff --git a/src/Std/Data/Iterators/Producers.lean b/src/Std/Data/Iterators/Producers.lean
new file mode 100644
index 0000000000..5053bfde4b
--- /dev/null
+++ b/src/Std/Data/Iterators/Producers.lean
@@ -0,0 +1,8 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+prelude
+import Std.Data.Iterators.Producers.Monadic
+import Std.Data.Iterators.Producers.List
diff --git a/src/Std/Data/Iterators/Producers/List.lean b/src/Std/Data/Iterators/Producers/List.lean
new file mode 100644
index 0000000000..1a630c58db
--- /dev/null
+++ b/src/Std/Data/Iterators/Producers/List.lean
@@ -0,0 +1,22 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+prelude
+import Std.Data.Iterators.Producers.Monadic.List
+
+/-!
+# List iterator
+
+This module provides an iterator for lists that is accessible via `List.iter`.
+-/
+
+namespace Std.Iterators
+
+@[always_inline, inline]
+def _root_.List.iter {α : Type w} (l : List α) :
+    Iter (α := ListIterator α) α :=
+  ((l.iterM Id).toPureIter : Iter α)
+
+end Std.Iterators
diff --git a/src/Std/Data/Iterators/Producers/Monadic.lean b/src/Std/Data/Iterators/Producers/Monadic.lean
new file mode 100644
index 0000000000..9c869fc322
--- /dev/null
+++ b/src/Std/Data/Iterators/Producers/Monadic.lean
@@ -0,0 +1,7 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+prelude
+import Std.Data.Iterators.Producers.Monadic.List
diff --git a/src/Std/Data/Iterators/Producers/Monadic/List.lean b/src/Std/Data/Iterators/Producers/Monadic/List.lean
new file mode 100644
index 0000000000..165741f2de
--- /dev/null
+++ b/src/Std/Data/Iterators/Producers/Monadic/List.lean
@@ -0,0 +1,76 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+prelude
+import Init.Data.Nat.Lemmas
+import Init.RCases
+import Std.Data.Iterators.Consumers
+import Std.Data.Iterators.Internal.Termination
+
+/-!
+# List iterator
+
+This module provides an iterator for lists that is accessible via `List.iterM`.
+-/
+
+namespace Std.Iterators
+
+variable {α : Type w} {m : Type w → Type w'}
+
+/--
+The underlying state of a list iterator. Its contents are internal and should
+not be used by downstream users of the library.
+-/
+structure ListIterator (α : Type w) where
+  list : List α
+
+/--
+Returns a finite iterator for the given list.
+The iterator yields the elements of the list in order and then terminates.
+-/
+@[always_inline, inline]
+def _root_.List.iterM {α : Type w} (l : List α) (m : Type w → Type w') [Pure m] :
+    IterM (α := ListIterator α) m α :=
+  toIterM { list := l } m α
+
+@[always_inline, inline]
+instance {α : Type w} [Pure m] : Iterator (ListIterator α) m α where
+  IsPlausibleStep it
+    | .yield it' out => it.internalState.list = out :: it'.internalState.list
+    | .skip _ => False
+    | .done => it.internalState.list = []
+  step it := pure (match it with
+        | ⟨⟨[]⟩⟩ => ⟨.done, rfl⟩
+        | ⟨⟨x :: xs⟩⟩ => ⟨.yield (toIterM ⟨xs⟩ m α) x, rfl⟩)
+
+private def ListIterator.finitenessRelation [Pure m] :
+    FinitenessRelation (ListIterator α) m where
+  rel := InvImage WellFoundedRelation.rel (ListIterator.list ∘ BaseIter.internalState)
+  wf := InvImage.wf _ WellFoundedRelation.wf
+  subrelation {it it'} h := by
+    simp_wf
+    obtain ⟨step, h, h'⟩ := h
+    cases step <;> simp_all [IterStep.successor, IterM.IsPlausibleStep, Iterator.IsPlausibleStep]
+
+instance [Pure m] : Finite (ListIterator α) m :=
+  Finite.of_finitenessRelation ListIterator.finitenessRelation
+
+@[always_inline, inline]
+instance {α : Type w} [Monad m] : IteratorCollect (ListIterator α) m :=
+  .defaultImplementation
+
+@[always_inline, inline]
+instance {α : Type w} [Monad m] : IteratorCollectPartial (ListIterator α) m :=
+  .defaultImplementation
+
+@[always_inline, inline]
+instance {α : Type w} [Monad m] [Monad n] : IteratorLoop (ListIterator α) m n :=
+  .defaultImplementation
+
+@[always_inline, inline]
+instance {α : Type w} [Monad m] [Monad n] : IteratorLoopPartial (ListIterator α) m n :=
+  .defaultImplementation
+
+end Std.Iterators
diff --git a/tests/lean/run/iterators.lean b/tests/lean/run/iterators.lean
new file mode 100644
index 0000000000..8ea779c51f
--- /dev/null
+++ b/tests/lean/run/iterators.lean
@@ -0,0 +1,67 @@
+import Std.Data.Iterators
+
+section ListIteratorBasic
+
+/-- info: [1, 2, 3].iter : Std.Iter Nat -/
+#guard_msgs in
+#check [1, 2, 3].iter
+
+/-- info: [1, 2, 3].iterM Id : Std.IterM Id Nat -/
+#guard_msgs in
+#check [1, 2, 3].iterM Id
+
+/-- info: [1, 2, 3] -/
+#guard_msgs in
+#eval [1, 2, 3].iter.toList
+
+/-- info: #[1, 2, 3] -/
+#guard_msgs in
+#eval [1, 2, 3].iter.toArray
+
+/-- info: [1, 2, 3] -/
+#guard_msgs in
+#eval [1, 2, 3].iter |>.allowNontermination.toList
+
+/-- info: ([1, 2, 3].iterM IO).toList : IO (List Nat) -/
+#guard_msgs in
+#check [1, 2, 3].iterM IO |>.toList
+
+/-- info: [1, 2, 3] -/
+#guard_msgs in
+#eval [1, 2, 3].iterM IO |>.toList
+
+/-- info: #[1, 2, 3] -/
+#guard_msgs in
+#eval [1, 2, 3].iterM IO |>.toArray
+
+end ListIteratorBasic
+
+section WellFoundedRecursion
+
+def sum (l : List Nat) : Nat :=
+  go l.iter 0
+where
+  @[specialize] -- The old code generator seems to need this.
+  go it acc :=
+    match it.step with
+    | .yield it' out _ => go it' (acc + out)
+    | .skip it' _ => go it' acc
+    | .done _ => acc
+  termination_by it.finitelyManySteps
+
+/-- info: 6 -/
+#guard_msgs in
+#eval sum [1, 2, 3]
+
+end WellFoundedRecursion
+
+section Loop
+
+def sumFold (l : List Nat) : Nat :=
+  l.iter.fold (init := 0) (· + ·)
+
+/-- info: 6 -/
+#guard_msgs in
+#eval [1, 2, 3].iter.fold (init := 0) (· + · )
+
+end Loop