instLawfulMonadContOptionT — Mathlib

Lean4

instance [MonadCont m] [LawfulMonadCont m] : LawfulMonadCont (OptionT m)
    where
  callCC_bind_right := by
    refine fun _ _ => OptionT.ext ?_
    simpa [callCC, Option.elimM, callCC_bind_right] using
      bind_congr fun
        | some _ => rfl
        | none => by simp [@callCC_dummy m _]
  callCC_bind_left := by
    intros
    simp only [callCC, OptionT.callCC, OptionT.goto_mkLabel, bind_pure_comp, OptionT.run_bind, OptionT.run_mk,
      Option.elimM_map, Option.elim_some, Function.comp_apply, @callCC_bind_left m _]
    ext; rfl
  callCC_dummy := by intros; simp only [callCC, OptionT.callCC, @callCC_dummy m _]; ext; rfl

Похожие утверждения