Mercurial > urweb
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 |