Commit 2023-06-18 08:20 b1242d93

View on Github →

feat: port Control.Monad.Cont (#4981)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Control/Monad/Cont.lean

added def Cont

added def ContT.equiv

added def ContT.map

added def ContT.monadLift

added theorem ContT.monadLift_bind

added def ContT.run

added theorem ContT.run_contT_map_contT

added theorem ContT.run_withContT

added def ContT.withContT

added def ContT

added theorem ExceptT.goto_mkLabel

added def ExceptT.mkLabel

added structure MonadCont.Label

added def MonadCont.goto

added theorem OptionT.goto_mkLabel

added def OptionT.mkLabel

added theorem ReaderT.goto_mkLabel

added def ReaderT.mkLabel

added theorem StateT.goto_mkLabel

added def StateT.mkLabel

added def WriterT.callCC'

added theorem WriterT.goto_mkLabel'

added theorem WriterT.goto_mkLabel

added def WriterT.mkLabel'

added def WriterT.mkLabel