%%% The Mini-ML typing rules. which can be used as a complete
%%% Author: Frank Pfenning
%%% Modified by Adam Poswolsky to be in declarative order.

of : exp -> tp -> type.  %name of P u.
ofscheme : tp -> tp -> tp -> type.

ofscheme_arrow : ofscheme (arrow T1 T2) T1 T2.
ofscheme_poly : {Targ} ofscheme (T Targ) T1 T2
                -> ofscheme (forall T) T1 T2.

% Natural Numbers
tp_z     : of z nat.
tp_s     : of E nat
            -> of (s E) nat.

tp_case  : of E1 nat
            -> of E2 T
            -> ({x:exp} of x nat -> of (E3 x) T)
            -> of (case E1 E2 E3) T.

% Pairs
tp_pair : of E1 T1
          -> of E2 T2
          -> of (pair E1 E2) (cross T1 T2).

tp_fst  : of E (cross T1 T2) -> of (fst E) T1.
tp_snd  : of E (cross T1 T2) -> of (snd E) T2.

% Functions
tp_lam : ({x:exp} of x T1 -> of (E x) T2)
          -> of (lam E) (arrow T1 T2).

tp_app : of E1 T
	  -> of E2 T1
          -> ofscheme T T1 T2
          -> of (app E1 E2) T2.

% Definitions
tp_letv :  of E1 T1
	   -> ({x:exp} of x T1 -> of (E2 x) T2)
           -> of (letv E1 E2) T2.
tp_letn :  of E1 T1
	   -> of (E2 E1) T2
           -> of (letn E1 E2) T2.

% Recursion
tp_fix : ({x:exp} of x T -> of (E x) T)
          -> of (fix E) T.

% Polymorphism
tp_polyintro : ({t:tp} of E (T t))
               -> of E (forall [t] (T t)).