r : int -> goalstack

SYNOPSIS

Reorders the subgoals on top of the subgoal package goal stack.

DESCRIPTION

The function r is part of the subgoal package. It `rotates' the current list of goals by the given number, which may be positive or negative. For a description of the subgoal package, see set_goal.

FAILURE CONDITIONS

If there are no goals.

EXAMPLE

  # g `(HD[1;2;3] = 1) /\ (TL[1;2;3] = [2;3]) /\ (HD (TL[1;2;3]) = 2)`;;
  val it : goalstack = 1 subgoal (1 total)

  `HD [1; 2; 3] = 1 /\ TL [1; 2; 3] = [2; 3] /\ HD (TL [1; 2; 3]) = 2`

  # e (REPEAT CONJ_TAC);;
  val it : goalstack = 3 subgoals (3 total)

  `HD (TL [1; 2; 3]) = 2`

  `TL [1; 2; 3] = [2; 3]`

  `HD [1; 2; 3] = 1`

  # r 1;;
  val it : goalstack = 1 subgoal (3 total)

  `TL [1; 2; 3] = [2; 3]`

  # r 1;;
  val it : goalstack = 1 subgoal (3 total)

  `HD (TL [1; 2; 3]) = 2`

USES

Proving subgoals in a different order from that generated by the subgoal package.

SEE ALSO

b, e, g, p, set_goal, top_thm.