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

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