Mercurial > urweb
comparison 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 |
comparison
equal
deleted
inserted
replaced
1286:829da30fb808 | 1287:5137b0537c92 |
---|---|
10 datatype bool = False | True | 10 datatype bool = False | True |
11 | 11 |
12 datatype option t = None | Some of t | 12 datatype option t = None | Some of t |
13 | 13 |
14 datatype list t = Nil | Cons of t * list t | 14 datatype list t = Nil | Cons of t * list t |
15 | |
16 | |
17 (** Polymorphic variants *) | |
18 | |
19 con variant :: {Type} -> Type | |
20 val make : nm :: Name -> t ::: Type -> ts ::: {Type} -> [[nm] ~ ts] => t -> variant ([nm = t] ++ ts) | |
21 val match : ts ::: {Type} -> t ::: Type -> variant ts -> $(map (fn t' => t' -> t) ts) -> t | |
15 | 22 |
16 | 23 |
17 (** Basic type classes *) | 24 (** Basic type classes *) |
18 | 25 |
19 class eq | 26 class eq |