--- a/variant.ur	Sun May 13 14:13:18 2012 -0400
+++ b/variant.ur	Thu Jul 26 16:39:02 2012 -0400
@@ -127,3 +127,19 @@
 fun makeEq [K] [f :: K -> Type] [nm :: Name] [t ::: K] [ts ::: {K}] [r ::: {K}] [[nm] ~ ts]
     (pf : Eq.eq r ([nm = t] ++ ts)) (x : f t) : variant (map f r) =
   Eq.cast (Eq.sym pf) [fn r => variant (map f r)] (make [nm] x)
+
+con variantMake ts' ts = $(map (fn t => t -> variant ts') ts)
+con mkLabelsAccum r = s :: {Type} -> [r ~ s] => variantMake (r ++ s) r
+fun mkLabels [ts ::: {Type}] (fl : folder ts) : variantMake ts ts
+  = @Top.fold [mkLabelsAccum]
+          (fn [nm::_] [v::_] [r::_] [[nm] ~ r]
+              (k : mkLabelsAccum r)
+              [s::_] [[nm = v] ++ r ~ s] => k [[nm = v] ++ s] ++ {nm = make [nm]})
+          (fn [s::_] [[] ~ s] => {}) fl [[]] !
+
+class type_case = fn ts t a => (a -> variant ts) -> a -> t
+
+fun declareCase [ts] [t] [a] (f : (a -> variant ts) -> a -> t) : type_case ts t a = f
+fun typeCase [ts] [t] (v : variant ts) (dstrs : $(map (type_case ts t) ts)) (fl : folder ts) : t
+(* Ur/Web not clever enough to calculate these folders, it seems *)
+  = match v (@ap [fn a => a -> variant ts] [fn a => a -> t] fl dstrs (@mkLabels fl))