ALL_TAC : tactic

SYNOPSIS

Passes on a goal unchanged.

DESCRIPTION

ALL_TAC applied to a goal g simply produces the subgoal list [g]. It is the identity for the THEN tactical.

FAILURE CONDITIONS

Never fails.

EXAMPLE

Suppose we want to solve the goal:

  # g `~(n MOD 2 = 0) <=> n MOD 2 = 1`;;
  ...

We could just solve it with e ARITH_TAC, but suppose we want to introduce a little lemma that n MOD 2 < 2, proving that by ARITH_TAC. We could do

  # e(SUBGOAL_THEN `n MOD 2 < 2` ASSUME_TAC THENL
       [ARITH_TAC;
        ...rest of proof...]);;

However if we split off many lemmas, we get a deeply nested proof structure that's a bit confusing. In cases where the proofs of the lemmas are trivial one-liners like this we might just want to keep the proof basically linear with

  # e(SUBGOL_THEN `n MOD 2 < 2` ASSUME_TAC THENL [ARITH_TAC; ALL_TAC] THEN
      ...rest of proof...);;

USES

Keeping proof structures linear, as in the above example, or convenient algebraic combinations in complicated tactic structures.

SEE ALSO

NO_TAC, REPEAT, THENL.