Commit 2022-11-30 17:39 8b5a89ee

View on Github →

feat: port Control.Monad.Basic (#752) mathlib SHA: 76171581280d5b5d1e2d1f4f37e5420357bdc636 Not sure what I need to do with the attributes. Also, should the type signatures be golfed in lean4 style?

Estimated changes

Modified Mathlib.lean

Created Mathlib/Control/Monad/Basic.lean

added def ReaderT.equiv

added def StateT.equiv

added def StateT.eval

added theorem map_eq_bind_pure_comp

Modified Mathlib/Control/SimpSet.lean