Mercurial > urweb
diff lib/ur/basis.urs @ 1287:5137b0537c92
Polymorphic variants
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Thu, 19 Aug 2010 17:28:52 -0400 |
parents | a9a500d22ebc |
children | 6791454653c5 |
line wrap: on
line diff
--- a/lib/ur/basis.urs Tue Aug 10 16:02:55 2010 -0400 +++ b/lib/ur/basis.urs Thu Aug 19 17:28:52 2010 -0400 @@ -14,6 +14,13 @@ 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