@[inline]

def Std.Iterators.Iter.Intermediate.dropWhile {β α : Type u_1} (P : β → Bool) (dropping : Bool) (it : Iter β) : Iter β

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

@[inline]

def Std.Iterators.Iter.dropWhile {α β : Type w} (P : β → Bool) (it : Iter β) : Iter β

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 if it is finite
• Productive instance: only if it 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.

Equations

• Std.Iterators.Iter.dropWhile P it = (Std.Iterators.IterM.dropWhile P it.toIterM).toIter