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