FAIL_TAC : string -> tactic
Tactic that always fails, with the supplied string.
Whatever goal it is applied to, FAIL_TAC "s" always fails with Failure "s".
- FAILURE CONDITIONS
The application of FAIL_TAC to a string never fails; the resulting
tactic always fails.
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:
# g `if x then T else T`;;
fails with the message provided, whereas the following quietly solves
# e(REWRITE_TAC THEN FAIL_TAC "Simple rewriting failed to solve goal");;
Exception: Failure "Simple rewriting failed to solve goal".
# e(REWRITE_TAC[COND_ID] THEN FAIL_TAC "Using that failed to solve goal");;
val it : goalstack = No subgoals
- SEE ALSO