Documentation

Std.Data.Iterators.Combinators.Monadic.Drop

This file provides the iterator combinator IterM.drop.

@[unbox]
structure Std.Iterators.Drop (α : Type w) (m : Type w → Type w') (β : Type w) :

The internal state of the IterM.drop combinator.

  • remaining : Nat

    Internal implementation detail of the iterator library

  • inner : IterM m β

    Internal implementation detail of the iterator library

Instances For
    @[inline]
    def Std.Iterators.IterM.drop {α : Type w} {m : Type w → Type w'} {β : Type w} (n : Nat) (it : IterM m β) :
    IterM m β

    Given an iterator it and a natural number n, it.drop n is an iterator that forwards all of it's output values except for the first n.

    Marble diagram:

    it          ---a----b---c--d-e--⊥
    it.drop 3   ---------------d-e--⊥
    
    it          ---a--⊥
    it.drop 3   ------⊥
    

    Termination properties:

    • Finite instance: only if it is finite
    • Productive instance: only if it is productive

    Performance:

    Currently, this combinator incurs an additional O(1) cost with each output of it, even when the iterator does not drop any elements anymore.

    Equations
    Instances For
      inductive Std.Iterators.Drop.PlausibleStep {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] (it : IterM m β) (step : IterStep (IterM m β) β) :
      Instances For
        instance Std.Iterators.Drop.instIterator {α : Type w} {m : Type w → Type w'} {β : Type w} [Monad m] [Iterator α m β] :
        Iterator (Drop α m β) m β
        Equations
        • One or more equations did not get rendered due to their size.
        instance Std.Iterators.Drop.instFinite {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] [Monad m] [Finite α m] :
        Finite (Drop α m β) m
        instance Std.Iterators.Drop.instProductive {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] [Monad m] [Productive α m] :
        Productive (Drop α m β) m