Constructs intermediate states of an iterator created with the combinator Iter.dropWhile
.
When it.dropWhile P
has stopped dropping elements, its new state cannot be created
directly with Iter.dropWhile
but only with Intermediate.dropWhile
.
Intermediate.dropWhile
is meant to be used only for internally or for verification purposes.
Equations
- Std.Iterators.Iter.Intermediate.dropWhile P dropping it = (Std.Iterators.IterM.Intermediate.dropWhile P dropping it.toIterM).toIter
Instances For
Given an iterator it
and a predicate P
, it.dropWhile P
is an iterator that
emits the values emitted by it
starting from the first value that is rejected by P
.
The elements before are dropped.
In situations where P
is monadic, use dropWhileM
instead.
Marble diagram:
Assuming that the predicate P
accepts a
and b
but rejects c
:
it ---a----b---c--d-e--⊥
it.dropWhile P ------------c--d-e--⊥
it ---a----⊥
it.dropWhile P --------⊥
Termination properties:
Finite
instance: only ifit
is finiteProductive
instance: only ifit
is finite
Depending on P
, it is possible that it.dropWhileM P
is productive although
it
is not. In this case, the Productive
instance needs to be proved manually.
Performance:
This combinator calls P
on each output of it
until the predicate evaluates to false. After
that, the combinator incurs an addictional O(1) cost for each value emitted by it
.