% Generalizing the language of goals to
% allow residuation of disjuction, failure, existential,
% and equality.

goal : type.
prog : type.
%name goal G.
%name prog D.

atom' : p -> goal.
and'  : goal -> goal -> goal.  %infix right 11 and'.
imp'  : prog -> goal -> goal.  %infix right 10 imp'.
true' : goal.
forall' : (i -> goal) -> goal.
or'   : goal -> goal -> goal.  %infix right 11 or'.
false'  : goal.
exists' : (i -> goal) -> goal.
==    : p -> p -> goal.        %infix none 12 ==.

atom^ : p -> prog.
and^  : prog -> prog -> prog.  %infix right 11 and^.
imp^  : goal -> prog -> prog.  %infix right 10 imp^.
true^ : prog.
forall^ : (i -> prog) -> prog.