Mercurial > urweb
comparison lib/ur/top.ur @ 1434:44f78d6fec29
Make 'ex' kind-generic
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Fri, 11 Mar 2011 18:36:24 -0500 |
parents | e8bea46f8eda |
children | 18d18a70821e |
comparison
equal
deleted
inserted
replaced
1433:66092ce45a76 | 1434:44f78d6fec29 |
---|---|
59 con snd3 = K1 ==> K2 ==> K3 ==> fn t :: (K1 * K2 * K3) => t.2 | 59 con snd3 = K1 ==> K2 ==> K3 ==> fn t :: (K1 * K2 * K3) => t.2 |
60 con thd3 = K1 ==> K2 ==> K3 ==> fn t :: (K1 * K2 * K3) => t.3 | 60 con thd3 = K1 ==> K2 ==> K3 ==> fn t :: (K1 * K2 * K3) => t.3 |
61 | 61 |
62 con mapU = K ==> fn f :: K => map (fn _ :: Unit => f) | 62 con mapU = K ==> fn f :: K => map (fn _ :: Unit => f) |
63 | 63 |
64 con ex = fn tf :: (Type -> Type) => | 64 con ex = K ==> fn tf :: (K -> Type) => |
65 res ::: Type -> (choice :: Type -> tf choice -> res) -> res | 65 res ::: Type -> (choice :: K -> tf choice -> res) -> res |
66 | 66 |
67 fun ex [tf :: (Type -> Type)] [choice :: Type] (body : tf choice) : ex tf = | 67 fun ex_intro [K] [tf :: K -> Type] [choice :: K] (body : tf choice) : ex tf = |
68 fn [res] (f : choice :: Type -> tf choice -> res) => | 68 fn [res] (f : choice :: K -> tf choice -> res) => |
69 f [choice] body | 69 f [choice] body |
70 | |
71 fun ex_elim [K] [tf ::: K -> Type] (v : ex tf) [res ::: Type] = @@v [res] | |
70 | 72 |
71 fun compose [t1 ::: Type] [t2 ::: Type] [t3 ::: Type] | 73 fun compose [t1 ::: Type] [t2 ::: Type] [t3 ::: Type] |
72 (f1 : t2 -> t3) (f2 : t1 -> t2) (x : t1) = f1 (f2 x) | 74 (f1 : t2 -> t3) (f2 : t1 -> t2) (x : t1) = f1 (f2 x) |
73 | 75 |
74 fun show_option [t ::: Type] (_ : show t) = | 76 fun show_option [t ::: Type] (_ : show t) = |