# Success If Fail With Message #

This file implements a tactic that succeeds only if its argument fails with a specified message.

It's mostly useful in tests, where we want to make sure that tactics fail in certain ways under circumstances.

source
def Mathlib.Tactic.successIfFailWithMsg :
Lean.ParserDescr

`success_if_fail_with_msg msg tacs` runs `tacs` and succeeds only if they fail with the message `msg`.

`msg` can be any term that evaluates to an explicit `String`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Tactic.successIfFailWithMessage {s α : Type} {m : Type → Type} [Monad m] [MonadLiftT BaseIO m] [MonadLiftT Lean.CoreM m] [Lean.MonadBacktrack s m] [Lean.MonadError m] (msg : String) (tacs : m α) (msgref ref : Option Lean.Syntax := none) :
m Unit

Evaluates `tacs` and succeeds only if `tacs` both fails and throws an error equal (as a string) to `msg`.

Equations

- One or more equations did not get rendered due to their size.

Instances For