SPLIT_LT

Tactical.SPLIT_LT : int -> list_tactic * list_tactic -> list_tactic

Splits a list of goals into two and applies a list-tactic to each part

For list-tactics ltac1 and ltac2, integer n and goal list gl, the application SPLIT_LT n (ltac1, ltac2) gl applies ltac1 to the first n goals in gl, and ltac2 to the remainder. If n is negative, ltac1 is applied to the goals before the last -n, and ltac2 to the last -n goals.

Failure

The application SPLIT_LT n (ltac1, ltac2) never fails, but when applied to a goal list, it fails if the index n is (in absolute value) larger then the length of the list, or if either of the list-tactics ltac1 and ltac2 fails.

Example

To apply tactic tac1 to a goal, and then to apply tac2 to all resulting subgoals except the first, use

  tac1 THEN_LT SPLIT_LT 1 (ALL_LT, ALLGOALS tac2)

See also

Tactical.THEN_LT, Tactical.ALL_LT, Tactical.ALLGOALS