ink

def successIfFail {M : Type → Type} {α : Type} [inst : Lean.MonadError M] [inst : Monad M] (m : M α) : M Lean.Exception

A generalisation of fail_if_success to an arbitrary MonadError.

Equations

• One or more equations did not get rendered due to their size.