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

@[unbox]

structure Std.Iterators.Types.StepSizeIterator (α : Type w) (m : Type w → Type w') (β : Type w) : Type w

• nextIdx : Nat
• n : Nat
• inner : IterM m β

instance Std.Iterators.instIteratorStepSizeIteratorOfIteratorAccessOfMonad {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [Iterator α m β] [IteratorAccess α m] [Monad m] : Iterator (Types.StepSizeIterator α m β) m β

def Std.Iterators.Types.StepSizeIterator.instFinitenessRelation {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [Iterator α m β] [IteratorAccess α m] [Monad m] [Finite α m] : FinitenessRelation (StepSizeIterator α m β) m

instance Std.Iterators.Types.StepSizeIterator.instFinite {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [Iterator α m β] [IteratorAccess α m] [Monad m] [Finite α m] : Finite (StepSizeIterator α m β) m

def Std.Iterators.Types.StepSizeIterator.instProductivenessRelation {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [Iterator α m β] [IteratorAccess α m] [Monad m] [Productive α m] : ProductivenessRelation (StepSizeIterator α m β) m

instance Std.Iterators.Types.StepSizeIterator.instProductive {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [Iterator α m β] [IteratorAccess α m] [Monad m] [Productive α m] : Productive (StepSizeIterator α m β) m

@[inline]

def Std.Iterators.IterM.stepSize {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [Iterator α m β] [IteratorAccess α m] [Monad m] (it : IterM m β) (n : Nat) : IterM m β

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

instance Std.Iterators.Types.StepSizeIterator.instIteratorCollect {α β : Type u_1} {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [Iterator α m β] [IteratorAccess α m] [Monad m] [Monad n] : IteratorCollect (StepSizeIterator α m β) m n

instance Std.Iterators.Types.StepSizeIterator.instIteratorCollectPartial {α β : Type u_1} {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [Iterator α m β] [IteratorAccess α m] [Monad m] [Monad n] : IteratorCollectPartial (StepSizeIterator α m β) m n

instance Std.Iterators.Types.StepSizeIterator.instIteratorLoop {α β : Type u_1} {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [Iterator α m β] [IteratorAccess α m] [Monad m] [Monad n] : IteratorLoop (StepSizeIterator α m β) m n

instance Std.Iterators.Types.StepSizeIterator.instIteratorLoopPartial {α β : Type u_1} {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [Iterator α m β] [IteratorAccess α m] [Monad m] [Monad n] : IteratorLoopPartial (StepSizeIterator α m β) m n

instance Std.Iterators.Types.StepSizeIterator.instIteratorSize {α β : Type u_1} {m : Type u_1 → Type u_2} [Iterator α m β] [IteratorAccess α m] [Monad m] [Finite (StepSizeIterator α m β) m] : IteratorSize (StepSizeIterator α m β) m

instance Std.Iterators.Types.StepSizeIterator.instIteratorSizePartial {α β : Type u_1} {m : Type u_1 → Type u_2} [Iterator α m β] [IteratorAccess α m] [Monad m] : IteratorSizePartial (StepSizeIterator α m β) m