Documentation

Mathlib.Lean.Exception

def successIfFail {M : TypeType} {α : 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.