def successIfFail {M : Type → Type} {α : Type} [Lean.MonadError M] [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.

def Lean.Exception.isFailedToSynthesize (e : Lean.Exception) : IO Bool

Check if an exception is a "failed to synthesize" exception.

These exceptions are raised in several different places, and the only commonality is the prefix of the string, so that's what we look for.

Equations

• e.isFailedToSynthesize = do let __do_lift ← e.toMessageData.toString pure (__do_lift.startsWith "failed to synthesize")