%%% Typing judgment using propositional formulas as types for proof terms.
%%% This illustrates the formulas-as-types paradigm.
%%% Author: Frank Pfenning

# : tm -> o -> type.
%infix none 9 #
%name # P Q

#pair : M # A
     -> N # B
     -> (pair M N) # (A and B).

#fst  : M # (A and B)
     -> fst M # A.

#snd  : M # (A and B)
     -> snd M # B.

#lam  : ({u:tm} u # A -> (M u) # B)
     -> (lam A M) # (A imp B).

#app  : M # (A imp B)
     -> N # A
     -> (app M N) # B.

#inl  : M # A
     -> (inl B M) # (A or B).

#inr  : N # B
     -> (inr A N) # (A or B).

#case : M # (A or B)
     -> ({u1:tm} u1 # A -> (N1 u1) # C)
     -> ({u2:tm} u2 # B -> (N2 u2) # C)
     -> (case M N1 N2) # C.

#mu   : ({p:o}{u:tm} u # A -> (M p u) # p)
     -> (mu A M) # (not A).

#mapp : M # (not A)
     -> N # A
     -> (mapp C M N) # C.

#triv : triv # true.

#abort : M # false
      -> (abort C M) # C.