FAIL_TAC : string -> tactic

SYNOPSIS

Tactic that always fails, with the supplied string.

DESCRIPTION

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.

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:

  # g `if x then T else T`;;

the tactic

  # e(REWRITE_TAC[] THEN FAIL_TAC "Simple rewriting failed to solve goal");;
  Exception: Failure "Simple rewriting failed to solve goal".

fails with the message provided, whereas the following quietly solves the goal:

  # e(REWRITE_TAC[COND_ID] THEN FAIL_TAC "Using that failed to solve goal");;
  val it : goalstack = No subgoals

SEE ALSO

ALL_TAC, NO_TAC.