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.

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.

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.