diff options
author | Adam Chlipala <adam@chlipala.net> | 2010-08-19 17:28:52 -0400 |
---|---|---|
committer | Adam Chlipala <adam@chlipala.net> | 2010-08-19 17:28:52 -0400 |
commit | 90f8d1bebc14a4a9153ffa9ec33c97f21cd0d560 (patch) | |
tree | 025b60966e74a3a00397814e167b4c71e1a63783 /lib | |
parent | 4caa8ade915e91da526320d5bde2440333fc8eb7 (diff) |
Polymorphic variants
Diffstat (limited to 'lib')
-rw-r--r-- | lib/ur/basis.urs | 7 |
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 |