theorem
Std.Iterators.Iter.step_take
{α β : Type u_1}
[Iterator α Id β]
{n : Nat}
{it : Iter β}
:
(take n it).step = match n with
| 0 => PlausibleIterStep.done ⋯
| k.succ =>
match it.step with
| ⟨IterStep.yield it' out, h⟩ => PlausibleIterStep.yield (take k it') out ⋯
| ⟨IterStep.skip it', h⟩ => PlausibleIterStep.skip (take (k + 1) it') ⋯
| ⟨IterStep.done, h⟩ => PlausibleIterStep.done ⋯
theorem
Std.Iterators.Iter.atIdxSlow?_take
{α β : Type u_1}
[Iterator α Id β]
[Productive α Id]
{k l : Nat}
{it : Iter β}
: