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