comparison lib/ur/top.ur @ 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
47 47
48 fun not b = if b then False else True 48 fun not b = if b then False else True
49 49
50 con idT (t :: Type) = t 50 con idT (t :: Type) = t
51 con record (t :: {Type}) = $t 51 con record (t :: {Type}) = $t
52 con fstTT (t :: (Type * Type)) = t.1 52 con fst = K1 ==> K2 ==> fn t :: (K1 * K2) => t.1
53 con sndTT (t :: (Type * Type)) = t.2 53 con snd = K1 ==> K2 ==> fn t :: (K1 * K2) => t.2
54 con fstTTT (t :: (Type * Type * Type)) = t.1 54 con fst3 = K1 ==> K2 ==> K3 ==> fn t :: (K1 * K2 * K3) => t.1
55 con sndTTT (t :: (Type * Type * Type)) = t.2 55 con snd3 = K1 ==> K2 ==> K3 ==> fn t :: (K1 * K2 * K3) => t.2
56 con thdTTT (t :: (Type * Type * Type)) = t.3 56 con thd3 = K1 ==> K2 ==> K3 ==> fn t :: (K1 * K2 * K3) => t.3
57 57
58 con mapUT = fn f :: Type => map (fn _ :: Unit => f) 58 con mapUT = fn f :: Type => map (fn _ :: Unit => f)
59 59
60 con ex = fn tf :: (Type -> Type) => 60 con ex = fn tf :: (Type -> Type) =>
61 res ::: Type -> (choice :: Type -> tf choice -> res) -> res 61 res ::: Type -> (choice :: Type -> tf choice -> res) -> res