theorem
Std.IterM.step_takeWhileWithPostcondition
{α : Type u_1}
{m : Type u_1 → Type u_2}
{β : Type u_1}
[Monad m]
[Iterator α m β]
{it : IterM m β}
{P : β → Iterators.PostconditionT m (ULift Bool)}
:
(takeWhileWithPostcondition P it).step = do
let __do_lift ← it.step
match __do_lift.inflate with
| ⟨IterStep.yield it' out, h⟩ => do
let __do_lift ← (P out).operation
match __do_lift with
| ⟨{ down := true }, h'⟩ =>
pure (Shrink.deflate (PlausibleIterStep.yield (takeWhileWithPostcondition P it') out ⋯))
| ⟨{ down := false }, h'⟩ => pure (Shrink.deflate (PlausibleIterStep.done ⋯))
| ⟨IterStep.skip it', h⟩ => pure (Shrink.deflate (PlausibleIterStep.skip (takeWhileWithPostcondition P it') ⋯))
| ⟨IterStep.done, h⟩ => pure (Shrink.deflate (PlausibleIterStep.done ⋯))
theorem
Std.IterM.step_takeWhileM
{α : Type u_1}
{m : Type u_1 → Type u_2}
{β : Type u_1}
[Monad m]
[MonadAttach m]
[LawfulMonad m]
[Iterator α m β]
{it : IterM m β}
{P : β → m (ULift Bool)}
:
(takeWhileM P it).step = do
let __do_lift ← it.step
match __do_lift.inflate with
| ⟨IterStep.yield it' out, h⟩ => do
let __do_lift ← MonadAttach.attach (P out)
match __do_lift with
| ⟨{ down := true }, hP⟩ => pure (Shrink.deflate (PlausibleIterStep.yield (takeWhileM P it') out ⋯))
| ⟨{ down := false }, hP⟩ => pure (Shrink.deflate (PlausibleIterStep.done ⋯))
| ⟨IterStep.skip it', h⟩ => pure (Shrink.deflate (PlausibleIterStep.skip (takeWhileM P it') ⋯))
| ⟨IterStep.done, h⟩ => pure (Shrink.deflate (PlausibleIterStep.done ⋯))
theorem
Std.IterM.step_takeWhile
{α : Type u_1}
{m : Type u_1 → Type u_2}
{β : Type u_1}
[Monad m]
[LawfulMonad m]
[Iterator α m β]
{it : IterM m β}
{P : β → Bool}
:
(takeWhile P it).step = do
let __do_lift ← it.step
match __do_lift.inflate with
| ⟨IterStep.yield it' out, h⟩ =>
match hP : P out with
| true => pure (Shrink.deflate (PlausibleIterStep.yield (takeWhile P it') out ⋯))
| false => pure (Shrink.deflate (PlausibleIterStep.done ⋯))
| ⟨IterStep.skip it', h⟩ => pure (Shrink.deflate (PlausibleIterStep.skip (takeWhile P it') ⋯))
| ⟨IterStep.done, h⟩ => pure (Shrink.deflate (PlausibleIterStep.done ⋯))