%%% 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

p : type. % Atoms

atom : p -> o.

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.