NO_TAC : tactic

SYNOPSIS

Tactic that always fails.

DESCRIPTION

Whatever goal it is applied to, NO_TAC always fails with Failure "NO_TAC".

FAILURE CONDITIONS

Always fails.

EXAMPLE

However trivial the goal, NO_TAC always fails:

  # g `T`;;
  val it : goalstack = 1 subgoal (1 total)

  `T`

  # e NO_TAC;;
  Exception: Failure "NO_TAC".

however, tac THEN NO_TAC will never reach NO_TAC if tac leaves no subgoals:

  # e(REWRITE_TAC[] THEN NO_TAC);;
  val it : goalstack = No subgoals

USES

Can be useful in forcing certain ``speculative'' tactics to fail unless they solve the goal completely. For example, you might wish to break down a huge conjunction of goals and attempt to solve as many conjuncts as possible by just rewriting with a list of theorems [thl]. You could do:

  REPEAT CONJ_TAC THEN REWRITE_TAC[thl]

However, if you don't want to apply the rewrites unless they result in an immediate solution, you can do instead:

  REPEAT CONJ_TAC THEN TRY(REWRITE_TAC[thl] THEN NO_TAC)

SEE ALSO

ALL_TAC, ALL_THEN, FAIL_TAC, NO_THEN.