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

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

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