%%% Language of formulas for intuitionistic and classical
%%% predicate calculus.
%%% Author: Frank Pfenning

i : type.  % individuals
%name i T S

o : type.  % formulas
%name o A B C

and    : o -> o -> o.  %infix right 11 and
imp    : o -> o -> o.  %infix right 10 imp
or     : o -> o -> o.  %infix right 11 or
not    : o -> o.       %prefix 12 not
true   : o.
false  : o.
forall : (i -> o) -> o.
exists : (i -> o) -> o.