summaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2010-08-19 17:28:52 -0400
committerGravatar Adam Chlipala <adam@chlipala.net>2010-08-19 17:28:52 -0400
commit90f8d1bebc14a4a9153ffa9ec33c97f21cd0d560 (patch)
tree025b60966e74a3a00397814e167b4c71e1a63783 /lib
parent4caa8ade915e91da526320d5bde2440333fc8eb7 (diff)
Polymorphic variants
Diffstat (limited to 'lib')
-rw-r--r--lib/ur/basis.urs7
1 files changed, 7 insertions, 0 deletions
diff --git a/lib/ur/basis.urs b/lib/ur/basis.urs
index f6141bc7..d9967d12 100644
--- a/lib/ur/basis.urs
+++ b/lib/ur/basis.urs
@@ -14,6 +14,13 @@ datatype option t = None | Some of t
datatype list t = Nil | Cons of t * list t
+(** Polymorphic variants *)
+
+con variant :: {Type} -> Type
+val make : nm :: Name -> t ::: Type -> ts ::: {Type} -> [[nm] ~ ts] => t -> variant ([nm = t] ++ ts)
+val match : ts ::: {Type} -> t ::: Type -> variant ts -> $(map (fn t' => t' -> t) ts) -> t
+
+
(** Basic type classes *)
class eq