The MR is the result of !488 (closed) and !501 (closed).
This adds the MThrow E M type class expresses the fact that the monad M allow error of type E to be thrown and any point with signature mthrow : E → M A. There is an alias MFail := MThrow unit and mfail := mthrow () for monads that can fail without any error payload like option.
This then replaces mguard with guard : P → {Decision P} → M P using mfail. The original guard notation disappears.
As such we've replaced guard P; mx with guard P;; mx in all lemmas. This MR further more replaces case_option_guard with a more general case_guard.
It also adds guard_or : E → P → {Decision P} → M P that throws an E instead of unit if P is false. Technically guard is just a notation for guard_or () like mfail and MFail.
These changes are very much breaking changes.
This is joint work with @adamAndMath.