ROTATE_LT
Tactical.ROTATE_LT : int -> list_tactic
Rotates a list of goals
ROTATE_LT n gl rotates a goal list gl by n places. For n >= 0,
this means moving the first n goals to the end of the list. A negative
n means rotating the list in the opposite direction.
Failure
Never fails.
Example
To bring the third goal to first position, leaving the others in order, use
SPLIT_LT 3 (ROTATE_LT ~1, ALL_LT)
Comments
Using SPLIT_LT, ROTATE_LT and REVERSE_LT, any reordering of a list
of goals is possible.
See also
proofManagerLib.rotate,
proofManagerLib.r,
Tactical.SPLIT_LT,
Tactical.REVERSE_LT,
Tactical.ALL_LT