21.2. Iterator Definitions

Iterators may be either monadic or pure, and they may be finite, productive, or potentially infinite. Monadic iterators use side effects in some monad to emit each value, and must therefore be used in the monad, while pure iterators do not require side effects. For example, iterating over all files in a directory requires the IO monad. Pure iterators have type Iter, while monadic iterators are represented by IterM.

structure

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

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

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

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

See Init.Data.Iterators.Consumers for ways to use an iterator. For example, it.toList will convert 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:

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

Instead the declaration type needs to be completely omitted:

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

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

Constructor

Std.Iterators.Iter.mk.{w}

Fields

internalState : α

Internal implementation detail of the iterator.

structure

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

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

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

See 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 β.

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

Instead the declaration type needs to be completely omitted:

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

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

Constructor

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

Fields

internalState : α

Internal implementation detail of the iterator.

The types Iter and IterM are merely wrappers around an internal state. This inner state type is the implicit parameter to the iterator types. For basic producer iterators, like the one that results from List.iter, this type is fairly simple; however, iterators that result from combinators use polymorphic state types that can grow large. Because Lean elaborates the specified return type of a function before elaborating its body, it may not be possible to automatically determine the internal state type of an iterator type returned by a function. In these cases, it can be helpful to omit the return type from the signature and instead place a type annotation on the definition's body, which allows the specific iterator combinators invoked from the body to be used to determine the state type.

Iterator State Types

Writing the internal state type explicitly for list and array iterators is feasible:

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

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

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

However, the internal state type of a use of the Iter.map combinator is quite complicated:

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

Omitting the state type leads to an error:

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

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

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

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

Rather than writing the state type by hand, it can be convenient to omit the return type and instead provide the annotation around the term:

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

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

Live ↪

The actual process of iteration consists of producing a sequence of iteration steps when requested. Each step returns an updated iterator with a new internal state along with either a data value (in IterStep.yield), an indicator that the caller should request a data value again (IterStep.skip), or an indication that iteration is finished (IterStep.done). Without the ability to skip, it would be much more difficult to work with iterator combinators such as Iter.filter that do not yield values for all of those yielded by the underlying iterator. With skip, the implementation of filter doesn't need to worry about whether the underlying iterator is finite in order to be a well-defined function, and reasoning about its finiteness can be carried out in separate proofs. Additionally, filter would require an inner loop, which is much more difficult for the compiler to inline.

inductive type

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

IterStep α β represents a step taken by an iterator (Iter β or IterM m β).

Constructors

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

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

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

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

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

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

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

Steps taken by Iter and IterM are respectively represented by the types Iter.Step and IterM.Step. Both types of step are wrappers around IterStep that include additional proofs that are used to track termination behavior.

def

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

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

def

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

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

Steps are produced from iterators using Iterator.step, which is a method of the Iterator type class. Iterator is used for both pure and monadic iterators; pure iterators can be completely polymorphic in the choice of monad, which allows callers to instantiate it with Id.

type class

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

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.

Instance Constructor

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

Methods

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

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

21.2.1. Plausibility🔗

In addition to the step function, instances of Iterator include a relation Iterator.IsPlausibleStep. This relation exists because most iterators both maintain invariants over their internal state and yield values in a predictable manner. For example, array iterators track both an array and a current index into it. Stepping an array iterator results in an iterator over the same underlying array; it yields a value when the index is small enough, or is done otherwise. The plausible steps from an iterator state are those which are related to it via the iterator's implementation of IsPlausibleStep. Tracking plausibility at the logical level makes it feasible to reason about termination behavior for monadic iterators.

Both Iter.Step and IterM.Step are defined in terms of PlausibleIterStep; thus, both types can be used with leading dot notation for its namespace. An Iter.Step or IterM.Step can be analyzed using the three match pattern functions PlausibleIterStep.yield, PlausibleIterStep.skip, and PlausibleIterStep.done. These functions pair the information in the underlying IterStep with the surrounding proof object.

def

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

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

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

def

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

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

def

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

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

def

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

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

21.2.2. Finite and Productive Iterators

Not all iterators are guaranteed to return a finite number of results; it is perfectly sensible to iterate over all of the natural numbers. Similarly, not all iterators are guaranteed to either return a single result or terminate; iterators may be defined using arbitrary programs. Thus, Lean divides iterators into three termination classes:

Finite iterators are guaranteed to finish iterating after a finite number of steps. These iterators have a Finite instance.
Productive iterators are guaranteed to yield a value or terminate in finitely many steps, but they may yield infinitely many values. These iterators have a Productive instance.
All other iterators, whose termination behavior is unknown. These iterators have neither instance.

All finite iterators are necessarily productive.

type class

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

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

Instance Constructor

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

Methods

wf : WellFounded IterM.IsPlausibleSuccessorOf

The relation of plausible successors is well-founded.

type class

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

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

Instance Constructor

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

Methods

wf : WellFounded IterM.IsPlausibleSkipSuccessorOf

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

Sometimes, a needed Finite instance is not available because an iterator has not yet been proved finite. In these cases, Iter.allowNontermination can be used to bypass a finiteness requirement.

def

Std.Iterators.Iter.allowNontermination.{w} {α β : Type w}
  (it : Iter β) : Iter.Partial β
Std.Iterators.Iter.allowNontermination.{w}
  {α β : Type w} (it : Iter β) :
  Iter.Partial β

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.

def

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

Iterating Over Nat

To write an iterator that yields each natural number in turn, the first step is to implement its internal state. This iterator only needs to remember the next natural number:

structure Nats where
  next : Nat

This iterator will only ever yield the next natural number. Thus, its step function will never return skip or done. Whenever it yields a value, the value will be the internal state's next field, and the successor iterator's next field will be one greater. The grind tactic suffices to show that the step is indeed plausible:

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

This step function is productive because it never returns skip. Thus, the proof that each chain of skips has finite length can rely on the fact that when it is a Nats iterator, Iterator.IsPlausibleStep it (.skip it') = False:

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

Because there are infinitely many Nats, the iterator is not finite.

A Nats iterator can be created using this function:

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

This iterator is useful with combinators such as Iter.zip:

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

0: cat
1: dog
2: pachycephalosaurus

Live ↪

Iterating Over Triples

The type Triple contains three values of the same type:

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

The internal state of an iterator over Triple can consist of a triple paired with a current position. This position may either be one of the fields or an indication that iteration is finished.

inductive TriplePos where
  | fst | snd | thd | done

Positions can be used to look up elements:

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

Each field's position has a successor position:

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

The iterator itself pairs a triple with the position of the next element:

structure TripleIterator α where
  triple : Triple α
  pos : TriplePos

Iteration begins at fst:

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

There are two plausible steps: either the iterator's position has a successor, in which case the next iterator is one that points at the same triple with the successor position, or it does not, in which case iteration is complete.

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

The corresponding step function yields the iterator and value describe by the relation:

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

This iterator cannot yet be converted to an array, because it is missing a Finite instance and an IteratorCollect instance:

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

#eval failed to synthesize instance of type class
  Finite (TripleIterator Char) Id

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

failed to synthesize instance of type class
  Finite (TripleIterator Char) Id

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

To prove finiteness, it's easiest to start at TriplePos.done and work backwards toward TriplePos.fst, showing that each position in turn has a finite chain of successors:

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

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

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

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

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

With the Finite instance in place, the default implementation of IteratorCollect can be used:

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

Iter.toArray now works:

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

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

To enable the iterator in Lean.Parser.Term.doFor : doElem`for x in e do s` iterates over `e` assuming `e`'s type has an instance of the `ForIn` typeclass. `break` and `continue` are supported inside `for` loops. `for x in e, x2 in e2, ... do s` iterates of the given collections in parallel, until at least one of them is exhausted. The types of `e2` etc. must implement the `Std.ToStream` typeclass.for loops, instances of IteratorLoopPartial and IteratorLoop are needed:

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

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

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

a
b
c

Live ↪

Iterators and Effects

One way to iterate over the contents of a file is to read a specified number of bytes from a Stream at each step. When EOF is reached, the iterator can close the file by letting its reference count drop to zero:

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

An iterator can be created by opening a file and converting its handle to a stream:

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

For this iterator, a yield is plausible when the file is still open, and done is plausible when the file is closed. The actual step function performs a read and closes the file if no bytes were returned:

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

To use it in loops, IteratorLoop and IteratorLoopPartial instances will be necessary. In practice, the latter is most important: because file streams may be infinite, the iterator itself may be infinite.

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

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

This is enough support code to use the iterator to calculate file sizes:

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

Live ↪

21.2.3. Accessing Elements

Some iterators support efficient random access. For example, an array iterator can skip any number of elements in constant time by incrementing the index that it maintains into the array.

type class

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

IteratorAccess α m provides efficient implementations for random access or iterators that support it. it.nextAtIdx? n either returns the step in which the n-th value of it is emitted (necessarily of the form .yield _ _) or .done if it terminates before emitting the n-th value.

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

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

Instance Constructor

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

Methods

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

def

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

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

This function is only available for iterators that explicitly support it by implementing the IteratorAccess typeclass.

21.2.4. Loops

type class

Std.Iterators.IteratorLoop.{w, w', x, x'} (α : Type w)
  (m : Type w → Type w') {β : Type w} [Iterator α m β]
  (n : Type x → Type x') : Type (max (max (max (w + 1) w') (x + 1)) x')
Std.Iterators.IteratorLoop.{w, w', x, x'}
  (α : Type w) (m : Type w → Type w')
  {β : Type w} [Iterator α m β]
  (n : Type x → Type x') :
  Type
    (max (max (max (w + 1) w') (x + 1))
        x')

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

Instance Constructor

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

Methods

forIn : ((γ : Type w) → (δ : Type x) → (γ → n δ) → m γ → n δ) →
  (γ : Type x) →
    (plausible_forInStep : β → γ → ForInStep γ → Prop) →
      IteratorLoop.WellFounded α m plausible_forInStep →
        (it : IterM m β) →
          γ → ((b : β) → it.IsPlausibleIndirectOutput b → (c : γ) → n (Subtype (plausible_forInStep b c))) → n γ

def

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

This is the default implementation of the IteratorLoop class. It simply iterates through the iterator using IterM.step. For certain iterators, more efficient implementations are possible and should be used instead.

type class

Std.Iterators.LawfulIteratorLoop.{w, w', x, x'} {β : Type w}
  (α : Type w) (m : Type w → Type w') (n : Type x → Type x') [Monad m]
  [Monad n] [Iterator α m β] [i : IteratorLoop α m n] : Prop
Std.Iterators.LawfulIteratorLoop.{w, w',
    x, x'}
  {β : Type w} (α : Type w)
  (m : Type w → Type w')
  (n : Type x → Type x') [Monad m]
  [Monad n] [Iterator α m β]
  [i : IteratorLoop α m n] : Prop

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

Instance Constructor

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

Methods

lawful : ∀ (lift : (γ : Type w) → (δ : Type x) → (γ → n δ) → m γ → n δ) [Std.Internal.LawfulMonadLiftBindFunction lift],
  IteratorLoop.forIn lift = IteratorLoop.forIn lift

type class

Std.Iterators.IteratorLoopPartial.{w, w', x, x'} (α : Type w)
  (m : Type w → Type w') {β : Type w} [Iterator α m β]
  (n : Type x → Type x') : Type (max (max (max (w + 1) w') (x + 1)) x')
Std.Iterators.IteratorLoopPartial.{w, w',
    x, x'}
  (α : Type w) (m : Type w → Type w')
  {β : Type w} [Iterator α m β]
  (n : Type x → Type x') :
  Type
    (max (max (max (w + 1) w') (x + 1))
        x')

IteratorLoopPartial α m provides efficient implementations of loop-based consumers for α-based iterators. The basis is a partial, i.e. potentially nonterminating, ForIn instance.

Instance Constructor

Std.Iterators.IteratorLoopPartial.mk.{w, w', x, x'}

Methods

forInPartial : ((γ : Type w) → (δ : Type x) → (γ → n δ) → m γ → n δ) →
  {γ : Type x} → (it : IterM m β) → γ → ((b : β) → it.IsPlausibleIndirectOutput b → γ → n (ForInStep γ)) → n γ

def

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

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.

21.2.5. Universe Levels

To make the universe levels of iterators more flexible, a wrapper type Shrink is applied around the result of Iterator.step. This type is presently a placeholder. It is present to reduce the scope of the breaking change when the full implementation is available.

def

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

Currently, Shrink α is just a wrapper around α.

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

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

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

def

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

Converts elements of Shrink α into elements of α.

def

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

Converts elements of α into elements of Shrink α.

21.2.6. Basic Iterators

In addition to the iterators provided by collection types, there are two basic iterators that are not connected to any underlying data structure. Iter.empty finishes iteration immediately after yielding no data, and Iter.repeat yields the same element forever. These iterators are primarily useful as parts of larger iterators built with combinators.

def

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

Returns an iterator that terminates immediately.

Termination properties:

Finite instance: always
Productive instance: always

def

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

Returns an iterator that terminates immediately.

Termination properties:

Finite instance: always
Productive instance: always

def

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

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

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

Termination properties:

Finite instance: not available and never possible
Productive instance: always