Additional methods for working with Exceptions

This file contains two additional methods for working with Exceptions

• successIfFail, a generalisation of fail_if_success to arbitrary MonadErrors
• isFailedToSynthesize: check if an exception is of the "failed to synthesize" form

def successIfFail {α : Type} {M : 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")