aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/ur/basis.urs
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
commit458bed0042d7bb206138ba6dce98686b056ae5c0 (patch)
tree025b60966e74a3a00397814e167b4c71e1a63783 /lib/ur/basis.urs
parent9da36d3a4dd89b2486b832384321c7a548ac67ca (diff)
Polymorphic variants
Diffstat (limited to 'lib/ur/basis.urs')
-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