theorem
Std.Iterators.Iter.step_intermediateDropWhile
{α β : Type u_1}
[Iterator α Id β]
{it : Iter β}
{P : β → Bool}
{dropping : Bool}
:
(Intermediate.dropWhile P dropping it).step = match it.step with
| ⟨IterStep.yield it' out, h⟩ =>
if h' : dropping = true then
match P out with
| true => PlausibleIterStep.skip (Intermediate.dropWhile P true it') ⋯
| false => PlausibleIterStep.yield (Intermediate.dropWhile P false it') out ⋯
else PlausibleIterStep.yield (Intermediate.dropWhile P false it') out ⋯
| ⟨IterStep.skip it', h⟩ => PlausibleIterStep.skip (Intermediate.dropWhile P dropping it') ⋯
| ⟨IterStep.done, h⟩ => PlausibleIterStep.done ⋯
theorem
Std.Iterators.Iter.step_dropWhile
{α β : Type u_1}
[Iterator α Id β]
{P : β → Bool}
{it : Iter β}
:
(dropWhile P it).step = match it.step with
| ⟨IterStep.yield it' out, h⟩ =>
match P out with
| true => PlausibleIterStep.skip (Intermediate.dropWhile P true it') ⋯
| false => PlausibleIterStep.yield (Intermediate.dropWhile P false it') out ⋯
| ⟨IterStep.skip it', h⟩ => PlausibleIterStep.skip (Intermediate.dropWhile P true it') ⋯
| ⟨IterStep.done, h⟩ => PlausibleIterStep.done ⋯
theorem
Std.Iterators.Iter.toList_intermediateDropWhile_of_finite
{α β : Type u_1}
[Iterator α Id β]
{P : β → Bool}
{dropping : Bool}
[Finite α Id]
[IteratorCollect α Id Id]
[LawfulIteratorCollect α Id Id]
{it : Iter β}
:
@[simp]
theorem
Std.Iterators.Iter.toList_dropWhile_of_finite
{α β : Type u_1}
[Iterator α Id β]
{P : β → Bool}
[Finite α Id]
[IteratorCollect α Id Id]
[LawfulIteratorCollect α Id Id]
{it : Iter β}
: