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

i : type.  % individuals
%name i T. % S % more than one currently disallowed

o : type.  % formulas
%name o A. % B C % more than one currently disallowed

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.