%%% A typed lambda-calculus that corresponds
%%% to the intuitionistic propositional fragment.
%%% It is used to illustrate the Curry-Howard isomorphism.
%%%
%%% Author: Frank Pfenning

tm : type.  % proof terms
%name tm M N

pair : tm -> tm -> tm.
fst  : tm -> tm.
snd  : tm -> tm.

lam  : o -> (tm -> tm) -> tm.
app  : tm -> tm -> tm.

inl  : o -> tm -> tm.
inr  : o -> tm -> tm.
case : tm -> (tm -> tm) -> (tm -> tm) -> tm.

mu   : o -> (o -> tm -> tm) -> tm.
mapp : o -> tm -> tm -> tm.

triv : tm.

abort : o -> tm -> tm.