NTAC

Tactic.NTAC : int -> tactic -> tactic

Apply tactic a specified number of times.

An invocation NTAC n tac applies the tactic tac exactly n times. If n <= 0 then the goal is unchanged.

Failure

Fails if tac fails.

Example

Suppose we have the following goal:

  ?- x = y

We apply a tactic for symmetry of equality 3 times:

  NTAC 3 (PURE_ONCE_REWRITE_TAC [EQ_SYM_EQ])

and obtain

  ?- y = x

Controlling iterated application tactics.

See also

Rewrite.PURE_ONCE_REWRITE_TAC, Tactical.REPEAT, Conv.REPEATC