%%% Intuitionistic propositional calculus
%%% Positive fragment with implies, and, true.
%%% Author: Frank Pfenning

% Type of propositions.
o : type.
%name o A.

% Type of atomic propositions.
atm : type.

% Syntax: implication, plus a few constants.
=> : o -> o -> o.  %infix right 10 =>.
&  : o -> o -> o.  %infix right 11 &.
true : o.
` : atm -> o.

% Atomic deductions (for faster search)
!^ : o -> type.
!v : o -> type.

trueI^ : !^ true.
andI^ : !^ A -> !^ B -> !^ (A & B).
andEvL : !v (A & B) -> !v A.
andEvR : !v (A & B) -> !v B.
impI^ : (!v A -> !^ B) -> !^ (A => B).
impEv : !v (A => B) -> !^ A -> !v B.
close : !v (` P) -> !^ (` P).