A reordering allows one to to reorder the subgoals generated by a
tactic, or reorder the prover’s active goals. Reorderings have the
type 'a reordering
, where 'a
is the tactic monad’s type
argument. Most reorderings are polymorphic.
signature REORDER =
sig
type 'a reordering
val reorder : 'a Tactic.tacticm -> 'a reordering -> 'a Tactic.tacticm
val id : 'a reordering
val swap : int -> int -> 'a reordering
val pull : int -> 'a reordering
val push : int -> 'a reordering
val rotateForward : int -> 'a reordering
val rotateBackward : int -> 'a reordering
val compose : 'a reordering list -> 'a reordering
val withCount : (int -> 'a reordering) -> 'a reordering
val contract : int -> 'a reordering
val sort : ('a -> 'a -> bool) -> 'a reordering
end
structure Reorder : REORDER
reorder tac reord
Uses reord
to reorder the subgoals generated by tac
.
(Goals can also be reordered at the top level using
Prover.reorder : Message.label Reorder.reordering -> unit
.)
swap i j
Swaps the first i
goals with the next j
goals.
pull i
Pulls the i
th goal to the front. Equivalent to swap i 1
.
push i
Pushes the first goal to the i
th position. Equivalent to swap 1 i
.
rotateForward i
Rotates goals i
positions toward the front. Equivalent to
withCount (fn n => swap i (n-i))
.
rotateBackward i
Rotates goals i
positions toward the back. Equivalent to
withCount (fn n => swap (n-i) i)
.
compose [r1, ..., rn]
Reorder with r1
, then r2
, etc.
withCount reord
If there are n
subgoals, equivalent to reord n
.
contract n
Contract the first n+1
goals (all of which must be identical) into
a single goal.
sort f
Place the goals in order from least to greatest, according to the
ordering given by f
.