REPEAT : tactic -> tactic

SYNOPSIS

Repeatedly applies a tactic until it fails.

DESCRIPTION

The tactic REPEAT t is a tactic which applies t to a goal, and while it succeeds, continues applying it to all subgoals generated.

FAILURE CONDITIONS

The application of REPEAT to a tactic never fails, and neither does the composite tactic, even if the basic tactic fails immediately, unless it raises an exception other that Failure ....

EXAMPLE

If we start with a goal having many universal quantifiers:

  # g `!w x y z. w < z /\ x < y ==> w * x + 1 <= y * z`;;

then GEN_TAC will strip them off one at a time:

  # e GEN_TAC;;
  val it : goalstack = 1 subgoal (1 total)

  `!x y z. w < z /\ x < y ==> w * x + 1 <= y * z`

and REPEAT GEN_TAC will strip them off as far as possible:

  # e(REPEAT GEN_TAC);;
  val it : goalstack = 1 subgoal (1 total)

  `w < z /\ x < y ==> w * x + 1 <= y * z`

Similarly, REPEAT COND_CASES_TAC will eliminate all free conditionals in the goal instead of just one.

SEE ALSO

EVERY, FIRST, ORELSE, THEN, THENL.