%%% The language and inference rules of natural deduction
%%% This contains only the positive fragment
%%% Author: Frank Pfenning

i : type.  % individuals
o : type.  % formulas
p : type.  % atomic formulas
%name i T. % S
%name o A. % B C
%name p P. % Q

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

pf : o -> type.  % natural deductions
%name pf D. % E

andi    : pf A -> pf B -> pf (A and B).
andel   : pf (A and B) -> pf A.
ander   : pf (A and B) -> pf B.

impi    : (pf A -> pf B) -> pf (A imp B).
impe    : pf (A imp B) -> pf A -> pf B.

truei   : pf (true).

foralli : ({a:i} pf (A a)) -> pf (forall A).
foralle : pf (forall A) -> {T:i} pf (A T).