def
successIfFail
{M : Type → Type}
{α : Type}
[inst : Lean.MonadError M]
[inst : Monad M]
(m : M α)
:
A generalisation of fail_if_success
to an arbitrary MonadError
.
Equations
- One or more equations did not get rendered due to their size.
Mathlib.Lean.Exception
A generalisation of fail_if_success
to an arbitrary MonadError
.