theorem
Std.Iterators.Take.isPlausibleStep_take_yield
{m : Type u_1 → Type u_2}
{α β : Type u_1}
{it' : IterM m β}
{out : β}
[Monad m]
[Iterator α m β]
{n : Nat}
{it : IterM m β}
(h : it.IsPlausibleStep (IterStep.yield it' out))
:
(IterM.take (n + 1) it).IsPlausibleStep (IterStep.yield (IterM.take n it') out)
theorem
Std.Iterators.Take.isPlausibleStep_take_skip
{m : Type u_1 → Type u_2}
{α β : Type u_1}
{it' : IterM m β}
[Monad m]
[Iterator α m β]
{n : Nat}
{it : IterM m β}
(h : it.IsPlausibleStep (IterStep.skip it'))
:
(IterM.take (n + 1) it).IsPlausibleStep (IterStep.skip (IterM.take (n + 1) it'))
theorem
Std.Iterators.IterM.step_take
{α : Type u_1}
{m : Type u_1 → Type u_2}
{β : Type u_1}
[Monad m]
[Iterator α m β]
{n : Nat}
{it : IterM m β}
:
(take n it).step = match n with
| 0 => pure (Shrink.deflate (PlausibleIterStep.done ⋯))
| k.succ => do
let __do_lift ← it.step
match __do_lift.inflate with
| ⟨IterStep.yield it' out, h⟩ => pure (Shrink.deflate (PlausibleIterStep.yield (take k it') out ⋯))
| ⟨IterStep.skip it', h⟩ => pure (Shrink.deflate (PlausibleIterStep.skip (take (k + 1) it') ⋯))
| ⟨IterStep.done, h⟩ => pure (Shrink.deflate (PlausibleIterStep.done ⋯))
theorem
Std.Iterators.IterM.step_toTake
{α : Type u_1}
{m : Type u_1 → Type u_2}
{β : Type u_1}
[Monad m]
[Iterator α m β]
[Finite α m]
{it : IterM m β}
:
it.toTake.step = do
let __do_lift ← it.step
match __do_lift.inflate with
| ⟨IterStep.yield it' out, h⟩ => pure (Shrink.deflate (PlausibleIterStep.yield it'.toTake out ⋯))
| ⟨IterStep.skip it', h⟩ => pure (Shrink.deflate (PlausibleIterStep.skip it'.toTake ⋯))
| ⟨IterStep.done, h⟩ => pure (Shrink.deflate (PlausibleIterStep.done ⋯))
@[simp]
theorem
Std.Iterators.IterM.toList_toTake
{α : Type u_1}
{m : Type u_1 → Type u_2}
{β : Type u_1}
[Monad m]
[LawfulMonad m]
[Iterator α m β]
[Finite α m]
[IteratorCollect α m m]
[LawfulIteratorCollect α m m]
{it : IterM m β}
: