Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-25 16:37:16 -0800 (Tue, 25 Jan 2005)
Revision: 6505
Log message:
This changes the sequent_arg in mmc_base_judgment to the following:
declare sequent [sequent_arg] { Univ[name:UnivClass,i:l] : Univ[name:UnivClass,i':l] >- Prop } : Judgment
where for convenience, we have the following:
iform unfold_exp : Exp <--> Univ["exp":t,0:l]
iform unfold_ty_exp : TyExp <--> Univ["exp":t,1:l]
iform unfold_kind_exp : KindExp <--> Univ["exp":t,2:l]
iform unfold_prop_exp : Prop <--> Univ["prop":t,1:l]
The parameter quantifiers are *within* the hyps clause (still
be added to the type checker).
declare sequent [sequent_arg] { (all name:t, all i:l.
Univ[name:UnivClass,i:l]
: Univ[name:UnivClass,i':l])
>- Prop } : Judgment
The non-disjoint union types make a lot of sense, but are impossible
to implement.
This solution preserves parametric polymorphism.