comparison lib/ur/top.urs @ 637:24fd1edfcaa3

Kind-polymorphic [fst] and friends
author Adam Chlipala <adamc@hcoop.net>
date Thu, 26 Feb 2009 16:16:54 -0500
parents 6c4643880df5
children aa2290c32ce2
comparison
equal deleted inserted replaced
636:de8333ef1a0c 637:24fd1edfcaa3
21 21
22 val not : bool -> bool 22 val not : bool -> bool
23 23
24 con idT = fn t :: Type => t 24 con idT = fn t :: Type => t
25 con record = fn t :: {Type} => $t 25 con record = fn t :: {Type} => $t
26 con fstTT = fn t :: (Type * Type) => t.1 26 con fst = K1 ==> K2 ==> fn t :: (K1 * K2) => t.1
27 con sndTT = fn t :: (Type * Type) => t.2 27 con snd = K1 ==> K2 ==> fn t :: (K1 * K2) => t.2
28 con fstTTT = fn t :: (Type * Type * Type) => t.1 28 con fst3 = K1 ==> K2 ==> K3 ==> fn t :: (K1 * K2 * K3) => t.1
29 con sndTTT = fn t :: (Type * Type * Type) => t.2 29 con snd3 = K1 ==> K2 ==> K3 ==> fn t :: (K1 * K2 * K3) => t.2
30 con thdTTT = fn t :: (Type * Type * Type) => t.3 30 con thd3 = K1 ==> K2 ==> K3 ==> fn t :: (K1 * K2 * K3) => t.3
31 31
32 con mapUT = fn f :: Type => map (fn _ :: Unit => f) 32 con mapUT = fn f :: Type => map (fn _ :: Unit => f)
33 33
34 con ex = fn tf :: (Type -> Type) => 34 con ex = fn tf :: (Type -> Type) =>
35 res ::: Type -> (choice :: Type -> tf choice -> res) -> res 35 res ::: Type -> (choice :: Type -> tf choice -> res) -> res