Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-29 21:14:14 -0800 (Sat, 29 Jan 2005)
Revision: 6525
Log message:
On the branch:
1. Union types are gone. For example,
sequent { A : B | C : D >- E } : F
2. They are replaced with a restricted form of dependent types.
declare typeclass TyHyp -> Ty
declare type A
declare type B : TyHyp
declare type C
declare type D : TyHyp
declare type Z{'ty : TyHyp} : Ty
declare rewrite Z{B} <--> A
declare rewrite Z{D} <--> C
declare sequent { Z{'a} : ('a :> TyHyp) >- Prop } : Judgment