FAIL_TAC
Tactical.FAIL_TAC : string -> tactic
Tactic which always fails, with the supplied string.
Whatever goal it is applied to, FAIL_TAC s always fails with the
string s.
Failure
The application of FAIL_TAC to a string never fails; the resulting
tactic always fails.
Example
The following example uses the fact that if a tactic t1 solves a goal,
then the tactic t1 THEN t2 never results in the application of t2 to
anything, because t1 produces no subgoals. In attempting to solve the
following goal:
?- if x then T else T
the tactic
REWRITE_TAC[] THEN FAIL_TAC "Simple rewriting failed to solve goal"
will fail with the message provided, whereas:
CONV_TAC COND_CONV THEN FAIL_TAC "Using COND_CONV failed to solve goal"
will silently solve the goal because COND_CONV reduces it to just
?- T.