theorem
Std.Iterators.IterM.dropWhileWithPostcondition_eq_intermediateDropWhileWithPostcondition
{α : Type u_1}
{m : Type u_1 → Type u_2}
{β : Type u_1}
[Iterator α m β]
{it : IterM m β}
{P : β → PostconditionT m (ULift Bool)}
:
theorem
Std.Iterators.IterM.step_intermediateDropWhileWithPostcondition
{α : Type u_1}
{m : Type u_1 → Type u_2}
{β : Type u_1}
[Monad m]
[Iterator α m β]
{it : IterM m β}
{P : β → PostconditionT m (ULift Bool)}
{dropping : Bool}
:
(Intermediate.dropWhileWithPostcondition P dropping it).step = do
let __do_lift ← it.step
match __do_lift with
| ⟨IterStep.yield it' out, h⟩ =>
if h' : dropping = true then do
let __do_lift ← (P out).operation
match __do_lift with
| ⟨{ down := true }, h''⟩ =>
pure (PlausibleIterStep.skip (Intermediate.dropWhileWithPostcondition P true it') ⋯)
| ⟨{ down := false }, h''⟩ =>
pure (PlausibleIterStep.yield (Intermediate.dropWhileWithPostcondition P false it') out ⋯)
else pure (PlausibleIterStep.yield (Intermediate.dropWhileWithPostcondition P false it') out ⋯)
| ⟨IterStep.skip it', h⟩ => pure (PlausibleIterStep.skip (Intermediate.dropWhileWithPostcondition P dropping it') ⋯)
| ⟨IterStep.done, h⟩ => pure (PlausibleIterStep.done ⋯)
theorem
Std.Iterators.IterM.step_dropWhileWithPostcondition
{α : Type u_1}
{m : Type u_1 → Type u_2}
{β : Type u_1}
[Monad m]
[Iterator α m β]
{it : IterM m β}
{P : β → PostconditionT m (ULift Bool)}
:
(dropWhileWithPostcondition P it).step = do
let __do_lift ← it.step
match __do_lift with
| ⟨IterStep.yield it' out, h⟩ => do
let __do_lift ← (P out).operation
match __do_lift with
| ⟨{ down := true }, h''⟩ =>
pure (PlausibleIterStep.skip (Intermediate.dropWhileWithPostcondition P true it') ⋯)
| ⟨{ down := false }, h''⟩ =>
pure (PlausibleIterStep.yield (Intermediate.dropWhileWithPostcondition P false it') out ⋯)
| ⟨IterStep.skip it', h⟩ => pure (PlausibleIterStep.skip (Intermediate.dropWhileWithPostcondition P true it') ⋯)
| ⟨IterStep.done, h⟩ => pure (PlausibleIterStep.done ⋯)
theorem
Std.Iterators.IterM.step_intermediateDropWhileM
{α : Type u_1}
{m : Type u_1 → Type u_2}
{β : Type u_1}
[Monad m]
[LawfulMonad m]
[Iterator α m β]
{it : IterM m β}
{P : β → m (ULift Bool)}
{dropping : Bool}
:
(Intermediate.dropWhileM P dropping it).step = do
let __do_lift ← it.step
match __do_lift with
| ⟨IterStep.yield it' out, h⟩ =>
if h' : dropping = true then do
let __do_lift ← P out
match __do_lift with
| { down := true } => pure (PlausibleIterStep.skip (Intermediate.dropWhileM P true it') ⋯)
| { down := false } => pure (PlausibleIterStep.yield (Intermediate.dropWhileM P false it') out ⋯)
else pure (PlausibleIterStep.yield (Intermediate.dropWhileM P false it') out ⋯)
| ⟨IterStep.skip it', h⟩ => pure (PlausibleIterStep.skip (Intermediate.dropWhileM P dropping it') ⋯)
| ⟨IterStep.done, h⟩ => pure (PlausibleIterStep.done ⋯)
theorem
Std.Iterators.IterM.step_dropWhileM
{α : Type u_1}
{m : Type u_1 → Type u_2}
{β : Type u_1}
[Monad m]
[LawfulMonad m]
[Iterator α m β]
{it : IterM m β}
{P : β → m (ULift Bool)}
:
(dropWhileM P it).step = do
let __do_lift ← it.step
match __do_lift with
| ⟨IterStep.yield it' out, h⟩ => do
let __do_lift ← P out
match __do_lift with
| { down := true } => pure (PlausibleIterStep.skip (Intermediate.dropWhileM P true it') ⋯)
| { down := false } => pure (PlausibleIterStep.yield (Intermediate.dropWhileM P false it') out ⋯)
| ⟨IterStep.skip it', h⟩ => pure (PlausibleIterStep.skip (Intermediate.dropWhileM P true it') ⋯)
| ⟨IterStep.done, h⟩ => pure (PlausibleIterStep.done ⋯)
theorem
Std.Iterators.IterM.step_intermediateDropWhile
{α : Type u_1}
{m : Type u_1 → Type u_2}
{β : Type u_1}
[Monad m]
[LawfulMonad m]
[Iterator α m β]
{it : IterM m β}
{P : β → Bool}
{dropping : Bool}
:
(Intermediate.dropWhile P dropping it).step = do
let __do_lift ← it.step
match __do_lift with
| ⟨IterStep.yield it' out, h⟩ =>
if h' : dropping = true then
match P out with
| true => pure (PlausibleIterStep.skip (Intermediate.dropWhile P true it') ⋯)
| false => pure (PlausibleIterStep.yield (Intermediate.dropWhile P false it') out ⋯)
else pure (PlausibleIterStep.yield (Intermediate.dropWhile P false it') out ⋯)
| ⟨IterStep.skip it', h⟩ => pure (PlausibleIterStep.skip (Intermediate.dropWhile P dropping it') ⋯)
| ⟨IterStep.done, h⟩ => pure (PlausibleIterStep.done ⋯)
theorem
Std.Iterators.IterM.step_dropWhile
{α : Type u_1}
{m : Type u_1 → Type u_2}
{β : Type u_1}
[Monad m]
[LawfulMonad m]
[Iterator α m β]
{it : IterM m β}
{P : β → Bool}
:
(dropWhile P it).step = do
let __do_lift ← it.step
match __do_lift with
| ⟨IterStep.yield it' out, h⟩ =>
match P out with
| true => pure (PlausibleIterStep.skip (Intermediate.dropWhile P true it') ⋯)
| false => pure (PlausibleIterStep.yield (Intermediate.dropWhile P false it') out ⋯)
| ⟨IterStep.skip it', h⟩ => pure (PlausibleIterStep.skip (Intermediate.dropWhile P true it') ⋯)
| ⟨IterStep.done, h⟩ => pure (PlausibleIterStep.done ⋯)