%  Tacticals provide a calculus for combining primitive tactics into
%  compound tactics.  Several tacticals are defined below.

module tacticals.
accumulate goals.

type idtac
     goal -> goal -> o.
type then, orelse, orelseC 
     (goal -> goal -> o) -> (goal -> goal -> o) -> goal -> goal -> o.
type repeat, try, complete
     (goal -> goal -> o) -> goal -> goal -> o.

idtac              In In.
then     Tac1 Tac2 In Out :- Tac1 In Mid, maptac Tac2 Mid Out.
orelse   Tac1 Tac2 In Out :- Tac1 In Out  ; Tac2 In Out.
orelseC  Tac1 Tac2 In Out :- Tac1 In Out,!; Tac2 In Out.
repeat   Tac       In Out :- orelse (then Tac (repeat Tac)) idtac In Out.
try      Tac       In Out :- orelse Tac idtac In Out.
complete Tac       In tt  :- Tac In Out, goalreduce Out tt.