source
@[irreducible, specialize #[]]
def Std.Iterators.Iter.atIdxSlow? {α β : Type u_1} [Iterator α Id β] [Productive α 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.

This function requires a `Productive` instance proving that the iterator will always emit a value after a finite number of skips. If the iterator is not productive or such an instance is not available, consider using `it.allowNontermination.atIdxSlow?` instead of `it.atIdxSlow?`. However, it is not possible to formally verify the behavior of the partial variant.

Equations

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

Instances For

source
@[specialize #[]]
partial def Std.Iterators.Iter.Partial.atIdxSlow? {α β : Type u_1} [Iterator α Id β] [Monad 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.

This is a partial, potentially nonterminating, function. It is not possible to formally verify its behavior. If the iterator has a `Productive` instance, consider using `Iter.atIdxSlow?` instead.

source
@[inline]
def Std.Iterators.Iter.atIdx? {α β : Type u_1} [Iterator α Id β] [Productive α 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

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

Instances For