Documentation

Mathlib.Lean.Exception

Additional methods for working with Exceptions #

This file contains two additional methods for working with Exceptions

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

    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_lifte.toMessageData.toString pure (__do_lift.startsWith "failed to synthesize")
    Instances For