Commit 2023-06-14 02:21 39293534

View on Github →

feat: port Init.Control.Lawful (#4999)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Control/Monad/Basic.lean

Modified Mathlib/Init/Align.lean

Created Mathlib/Init/Control/Lawful.lean

added theorem ExceptT.run_mk

added theorem ExceptT.run_monadLift

added theorem ExceptT.run_monadMap

added theorem OptionT.ext

added theorem OptionT.run_bind

added theorem OptionT.run_map

added theorem OptionT.run_mk

added theorem OptionT.run_monadLift

added theorem OptionT.run_monadMap

added theorem OptionT.run_pure

added theorem ReaderT.run_mk

added theorem StateT.run_mk