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