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

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