@[specialize #[]]

def Std.Iter.atIdxSlow? {α β : Type u_1} [Iterator α Id β] (n : Nat) (it : Iter β) : Option β

If possible, takes n steps with the iterator it and returns the n-th emitted value, or none if it finished before emitting n values.

If the iterator is not productive, this function might run forever in an endless loop of iterator steps. The variant it.ensureTermination.atIdxSlow? is guaranteed to terminate after finitely many steps.

Equations

• One or more equations did not get rendered due to their size.

theorem Std.Iter.atIdxSlow?.induct_unfolding {α β : Type u} [Iterator α Id β] [Iterators.Productive α Id] (motive : Nat → Iter β → Option β → Prop) (yield_zero : ∀ (it it' : Iter β) (out : β) (property : it.IsPlausibleStep (IterStep.yield it' out)), it.step = ⟨IterStep.yield it' out, property⟩ → motive 0 it (some out)) (yield_succ : ∀ (it it' : Iter β) (out : β) (property : it.IsPlausibleStep (IterStep.yield it' out)), it.step = ⟨IterStep.yield it' out, property⟩ → ∀ (k : Nat), motive k it' (atIdxSlow? k it') → motive k.succ it (atIdxSlow? k it')) (skip_case : ∀ (n : Nat) (it it' : Iter β) (property : it.IsPlausibleStep (IterStep.skip it')), it.step = ⟨IterStep.skip it', property⟩ → motive n it' (atIdxSlow? n it') → motive n it (atIdxSlow? n it')) (done_case : ∀ (n : Nat) (it : Iter β) (property : it.IsPlausibleStep IterStep.done), it.step = ⟨IterStep.done, property⟩ → motive n it none) (n : Nat) (it : Iter β) : motive n it (atIdxSlow? n it)

An induction principle for Iter.atIdxSlow?.

This lemma provides a functional induction principle for reasoning about Iter.atIdxSlow? n it.

The induction follows the structure of iterator steps.

• base case: when we reach the desired index (n = 0) and get a .yield step
• inductive case: when we have a .yield step but need to continue (n > 0)
• skip case: when we encounter a .skip step and continue with the same index
• done case: when the iterator is exhausted and we return none

@[inline]

def Std.Iter.Total.atIdxSlow? {α β : Type u_1} [Iterator α Id β] [Iterators.Productive α Id] (n : Nat) (it : Total β) : Option β

If possible, takes n steps with the iterator it and returns the n-th emitted value, or none if it finished before emitting n values.

This variant terminates after finitely many steps and requires a proof that the iterator is productive. If such a proof is not available, consider using Iter.toArray.

Equations

• Std.Iter.Total.atIdxSlow? n it = Std.Iter.atIdxSlow? n it.it

@[inline, deprecated Std.Iter.atIdxSlow? (since := "2026-01-28")]

def Std.Iter.Partial.atIdxSlow? {α β : Type u_1} [Iterator α Id β] (n : Nat) (it : Partial β) : Option β

If possible, takes n steps with the iterator it and returns the n-th emitted value, or none if it finished before emitting n values.

If the iterator is not productive, this function might run forever in an endless loop of iterator steps. The variant it.ensureTermination.atIdxSlow? is guaranteed to terminate after finitely many steps.

Equations

• Std.Iter.Partial.atIdxSlow? n it = Std.Iter.atIdxSlow? n it.it

@[inline]

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

Returns the n-th value emitted by it, or none if it terminates earlier.

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

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

Equations

• Std.Iter.atIdx? n it = match (Std.IteratorAccess.nextAtIdx? it.toIterM n).run.val with | Std.IterStep.yield it out => some out | Std.IterStep.skip it => none | Std.IterStep.done => none