theorem
Std.Iterators.Iter.step_takeWhile
{α β : Type u_1}
[Iterator α Id β]
{P : β → Bool}
{it : Iter β}
:
(takeWhile P it).step = match it.step with
| ⟨IterStep.yield it' out, h⟩ =>
match P out with
| true => PlausibleIterStep.yield (takeWhile P it') out ⋯
| false => PlausibleIterStep.done ⋯
| ⟨IterStep.skip it', h⟩ => PlausibleIterStep.skip (takeWhile P it') ⋯
| ⟨IterStep.done, h⟩ => PlausibleIterStep.done ⋯
theorem
Std.Iterators.Iter.atIdxSlow?_takeWhile
{α β : Type u_1}
[Iterator α Id β]
[Productive α Id]
{l : Nat}
{it : Iter β}
{P : β → Bool}
:
atIdxSlow? l (takeWhile P it) = if ∀ (k : Nat), k ≤ l → Option.any P (atIdxSlow? k it) = true then atIdxSlow? l it else none
@[simp]
theorem
Std.Iterators.Iter.toList_takeWhile_of_finite
{α β : Type u_1}
[Iterator α Id β]
{P : β → Bool}
[Finite α Id]
[IteratorCollect α Id Id]
[LawfulIteratorCollect α Id Id]
{it : Iter β}
:
@[simp]
theorem
Std.Iterators.Iter.toArray_takeWhile_of_finite
{α β : Type u_1}
[Iterator α Id β]
{P : β → Bool}
[Finite α Id]
[IteratorCollect α Id Id]
[LawfulIteratorCollect α Id Id]
{it : Iter β}
: