Documentation

Mathlib.Tactic.SuccessIfFailWithMsg

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.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    def Mathlib.Tactic.successIfFailWithMessage {s : Type} {α : Type} {m : TypeType} [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.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For