@[inline]

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

Given an iterator it and a predicate P, it.takeWhile P is an iterator that outputs the values emitted by it until one of those values is rejected by P. If some emitted value is rejected by P, the value is dropped and the iterator terminates.

Marble diagram:

Assuming that the predicate P accepts a and b but rejects c:

it               ---a----b---c--d-e--⊥
it.takeWhile P   ---a----b---⊥

it               ---a----⊥
it.takeWhile P   ---a----⊥

Termination properties:

• Finite instance: only if it is finite
• Productive instance: only if it is productive

Depending on P, it is possible that it.takeWhile P is finite (or productive) although it is not. In this case, the Finite (or Productive) instance needs to be proved manually.

Performance:

This combinator calls P on each output of it until the predicate evaluates to false. Then it terminates.