This file provides the iterator combinator IterM.drop
.
@[unbox]
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 ifit
is finiteProductive
instance: only ifit
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.Iterators.IterM.drop n it = Std.Iterators.toIterM { remaining := n, inner := it } m β
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 β) β)
:
- 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)
Instances For
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.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