source
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`.

Instances For

source
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')
source
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))

Instances

source
@[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

Instances For

source
@[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.

Instances For