lean4-htt/src/Std/Do
Sebastian Graf ba52e9393c
feat: LawfulMonad and WPMonad instances for Option and OptionT (#9932)
This PR adds `LawfulMonad` and `WPMonad` instances for `Option` and
`OptionT`.
2025-10-01 16:16:07 +00:00
..
SPred chore: split Std.Do.SPred.Notation in preparation for meta semantics restrictions (#10358) 2025-09-12 11:09:26 +00:00
Triple feat: introduce List.Cursor.pos as an abbreviation for prefix.length (#10642) 2025-10-01 15:28:30 +00:00
WP feat: LawfulMonad and WPMonad instances for Option and OptionT (#9932) 2025-10-01 16:16:07 +00:00
PostCond.lean feat: implement Std.Do.Triple.mp (#9931) 2025-08-15 17:44:15 +00:00
PredTrans.lean feat: LawfulMonad and WPMonad instances for Option and OptionT (#9932) 2025-10-01 16:16:07 +00:00
SPred.lean refactor: module-ize remainder of Std (#9195) 2025-07-17 11:43:57 +00:00
Triple.lean refactor: module-ize remainder of Std (#9195) 2025-07-17 11:43:57 +00:00
WP.lean refactor: module-ize remainder of Std (#9195) 2025-07-17 11:43:57 +00:00