theorem Std.Iterators.Types.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.Types.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.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.IterM.toList_take_zero {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterators.Finite (Iterators.Types.Take α m) m] {it : IterM m β} :
theorem Std.IterM.step_toTake {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] [Iterator α m β] [Iterators.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.IterM.toList_toTake {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterators.Finite α m] {it : IterM m β} :