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.

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.

Instances For
    def Mathlib.Tactic.successIfFailWithMessage {m : TypeType} {s : Type} {α : Type} [Monad m] [MonadLiftT IO m] [Lean.MonadBacktrack s m] [Lean.MonadError m] (msg : String) (tacs : m α) (ref : optParam (Option Lean.Syntax) none) :

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

    Instances For