Commit 2026-04-27 15:18 c58be837

feat: missing lemmas for ContT.run (#38379) This PR also adds ContT.mk (f : (α → m r) → m r) : ContT r m α := f for explicitly constructing a ContT action from a function that requires a callback, which allows a run_mk lemmas to eliminate ContT entirely from certain terms. This also makes MonadCont.goto an abbrev, to avoid needing a lemma about MonadCont.goto (Label.mk goto) = goto.