This file provides the iterator combinator IterM.drop.

@[unbox]

structure Std.Iterators.Drop (α : Type w) (m : Type w → 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

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

inductive Std.Iterators.Drop.PlausibleStep {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] (it : IterM m β) (step : IterStep (IterM m β) β) : Prop

• drop {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] {it : IterM m β} {it' : IterM m β} {out : β} {k : Nat} : it.internalState.inner.IsPlausibleStep (IterStep.yield it' out) → it.internalState.remaining = k + 1 → PlausibleStep it (IterStep.skip (IterM.drop k it'))
• skip {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] {it : IterM m β} {it' : IterM m β} : it.internalState.inner.IsPlausibleStep (IterStep.skip it') → PlausibleStep it (IterStep.skip (IterM.drop it.internalState.remaining it'))
• done {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] {it : IterM m β} : it.internalState.inner.IsPlausibleStep IterStep.done → PlausibleStep it IterStep.done
• yield {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] {it : IterM m β} {it' : IterM m β} {out : β} : it.internalState.inner.IsPlausibleStep (IterStep.yield it' out) → it.internalState.remaining = 0 → PlausibleStep it (IterStep.yield (IterM.drop 0 it') out)

instance Std.Iterators.Drop.instIterator {α : Type w} {m : Type w → Type w'} {β : Type w} [Monad m] [Iterator α m β] : Iterator (Drop α m β) m β

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

instance Std.Iterators.Drop.instIteratorCollect {α : Type w} {m : Type w → Type w'} {β : Type w} {n : Type w → Type u_1} [Monad m] [Monad n] [Iterator α m β] [Finite α m] : IteratorCollect (Drop α m β) m n

instance Std.Iterators.Drop.instIteratorCollectPartial {α : Type w} {m : Type w → Type w'} {β : Type w} {n : Type w → Type u_1} [Monad m] [Monad n] [Iterator α m β] : IteratorCollectPartial (Drop α m β) m n

instance Std.Iterators.Drop.instIteratorLoop {α : Type w} {m : Type w → Type w'} {β : Type w} {n : Type w → Type u_1} [Monad m] [Monad n] [Iterator α m β] : IteratorLoop (Drop α m β) m n

instance Std.Iterators.Drop.instIteratorLoopPartial {α : Type w} {m : Type w → Type w'} {β : Type w} {n : Type w → Type u_1} [Monad m] [Monad n] [Iterator α m β] : IteratorLoopPartial (Drop α m β) m n

instance Std.Iterators.instIteratorSizeDropOfFiniteOfIteratorLoop {m : Type w → Type w'} {β α : Type w} [Monad m] [Iterator α m β] [Finite α m] [IteratorLoop α m m] : IteratorSize (Drop α m β) m

instance Std.Iterators.instIteratorSizePartialDropOfIteratorLoopPartial {m : Type w → Type w'} {β α : Type w} [Monad m] [Iterator α m β] [IteratorLoopPartial α m m] : IteratorSizePartial (Drop α m β) m