This module provides a combinator that only yields every n-th element of another iterator.

@[inline]

def Std.Iter.stepSize {α β : Type u_1} [Iterator α Id β] [IteratorAccess α Id] (it : Iter β) (n : Nat) : Iter β

Produces an iterator that emits one value of it, then drops n - 1 elements, then emits another value, and so on. In other words, it emits every n-th value of it, starting with the first one.

If n = 0, the iterator behaves like for n = 1: It emits all values of it.

Marble diagram:

it               ---1----2----3---4----5
it.stepSize 2    ---1---------3--------5

Availability:

This operation is currently only available for iterators implementing IteratorAccess, such as PRange.iter range iterators.

Termination properties:

• Finite instance: only if the base iterator it is finite
• Productive instance: always

Equations

• it.stepSize n = (it.toIterM.stepSize n).toIter