Documentation

Std.Data.Iterators.Combinators.Monadic.StepSize

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

source
@[unbox]
structure Std.Iterators.Types.StepSizeIterator (α : Type w) (m : Type w → Type w') (β : Type w) :
Type w
Instances For
    source
    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 β
    Equations
    • One or more equations did not get rendered due to their size.
    source
    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
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      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
      source
      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
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        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
        source
        @[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
        Equations
        • it.stepSize n = { internalState := { nextIdx := 0, n := n - 1, inner := it } }
        Instances For
          source
          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
          Equations
          source
          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
          Equations
          source
          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
          Equations
          source
          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
          Equations
          source
          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
          Equations
          source
          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
          Equations