This file provides the iterator combinator IterM.drop.

@[unbox]

structure Std.Iterators.Types.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

@[implicit_reducible, inline]

def Std.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

• Std.IterM.drop n it = { internalState := { remaining := n, inner := it } }

inductive Std.Iterators.Types.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_reducible]

instance Std.Iterators.Types.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.Types.Drop.instFinite {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] [Monad m] [Finite α m] : Finite (Drop α m β) m

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

@[instance_reducible]

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

Equations

• Std.Iterators.Types.Drop.instIteratorLoop = Std.IteratorLoop.defaultImplementation