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 : Type → Type}
[Monad m]
[MonadLiftT IO m]
[Lean.MonadBacktrack s m]
[Lean.MonadError m]
(msg : String)
(tacs : m α)
(ref : optParam (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.