inductive Std.Iterators.IterM.IsPlausibleNthOutputStep {α β : Type w} {m : Type w → Type w'} [Iterator α m β] : Nat → IterM m β → IterStep (IterM m β) β → Prop

it.IsPlausibleNthOutputStep n step is the proposition that according to the IsPlausibleStep relation, it is plausible that step returns the step in which the n-th value of it is emitted, or .done if it can plausibly terminate before emitting n values.

• zero_yield {α β : Type w} {m : Type w → Type w'} [Iterator α m β] {it' : IterM m β} {out : β} {it : IterM m β} : it.IsPlausibleStep (IterStep.yield it' out) → IsPlausibleNthOutputStep 0 it (IterStep.yield it' out)

  If it plausibly yields in its immediate next step, this step is a plausible 0-th output step.

• done {α β : Type w} {m : Type w → Type w'} [Iterator α m β] {n : Nat} {it : IterM m β} : it.IsPlausibleStep IterStep.done → IsPlausibleNthOutputStep n it IterStep.done

  If it plausibly terminates in its immediate next step (.done), then .done is a plausible n-th output step for arbitrary n.

• yield {α β : Type w} {m : Type w → Type w'} [Iterator α m β] {n : Nat} {it it' : IterM m β} {out : β} {step : IterStep (IterM m β) β} : it.IsPlausibleStep (IterStep.yield it' out) → IsPlausibleNthOutputStep n it' step → IsPlausibleNthOutputStep (n + 1) it step

  If it plausibly yields in its immediate next step, the successor iterator being it', and if step is a plausible n-th output step of it', then step is a plausible n + 1-th output step of it.

• skip {α β : Type w} {m : Type w → Type w'} [Iterator α m β] {n : Nat} {it it' : IterM m β} {step : IterStep (IterM m β) β} : it.IsPlausibleStep (IterStep.skip it') → IsPlausibleNthOutputStep n it' step → IsPlausibleNthOutputStep n it step

  If it plausibly skips in its immediate next step, the successor iterator being it', and if step is a plausible n-th output step of it', then step is also a plausible n-th output step of it.

theorem Std.Iterators.IterM.not_isPlausibleNthOutputStep_yield {α β : Type w} {m : Type w → Type w'} [Iterator α m β] {n : Nat} {it it' : IterM m β} : ¬IsPlausibleNthOutputStep n it (IterStep.skip it')

class Std.Iterators.IteratorAccess (α : 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.

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

@[inline]

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

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

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

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

Equations

• it.nextAtIdx? n = Std.Iterators.IteratorAccess.nextAtIdx? it n

@[inline]

def Std.Iterators.IterM.atIdx? {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [Iterator α m β] [IteratorAccess α m] [Monad m] (it : IterM m β) (n : Nat) : m (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

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