--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/variant.urs	Tue Dec 14 10:33:24 2010 -0500
@@ -0,0 +1,33 @@
+(** Derived functions dealing with polymorphic variants *)
+
+val read : r ::: {Unit} -> t ::: Type -> folder r -> $(mapU t r) -> variant (mapU {} r) -> t
+val write : r ::: {Unit} -> t ::: Type -> folder r -> $(mapU t r) -> variant (mapU {} r) -> t -> $(mapU t r)
+
+val search : r ::: {Unit} -> t ::: Type -> (variant (mapU {} r) -> option t) -> folder r -> option t
+val find : r ::: {Unit} -> (variant (mapU {} r) -> bool) -> folder r -> option (variant (mapU {} r))
+
+val test : nm :: Name -> t ::: Type -> ts ::: {Type} -> [[nm] ~ ts] => folder ([nm = t] ++ ts)
+                                                                    -> variant ([nm = t] ++ ts) -> option t
+val testLess : nm :: Name -> t ::: Type -> ts ::: {Type} -> [[nm] ~ ts] => folder ts -> variant ([nm = t] ++ ts) -> option t
+
+val testEq : K --> f :: (K -> Type) -> nm :: Name -> t ::: K -> ts ::: {K} -> r ::: {K} -> [[nm] ~ ts] =>
+    Eq.eq r ([nm = t] ++ ts)
+    -> folder r
+    -> variant (map f r) -> option (f t)
+
+val eq : r ::: {Unit} -> folder r -> variant (mapU {} r) -> variant (mapU {} r) -> bool
+
+val makeEq : K --> f :: (K -> Type) -> nm :: Name -> t ::: K -> ts ::: {K} -> r ::: {K} -> [[nm] ~ ts] =>
+    Eq.eq r ([nm = t] ++ ts)
+    -> f t
+    -> variant (map f r)
+
+val fold : r ::: {Unit} -> t ::: Type -> folder r -> (variant (mapU {} r) -> t -> t) -> t -> t
+
+val destrR : K --> f :: (K -> Type) -> fr :: (K -> Type) -> t ::: Type
+             -> (p :: K -> f p -> fr p -> t)
+             -> r ::: {K} -> folder r -> variant (map f r) -> $(map fr r) -> t
+
+val destr2R : K --> f1 :: (K -> Type) -> f2 :: (K -> Type) -> fr :: (K -> Type) -> t ::: Type
+             -> (p :: K -> f1 p -> f2 p -> fr p -> t)
+             -> r ::: {K} -> folder r -> variant (map f1 r) -> variant (map f2 r) -> $(map fr r) -> option t