Mercurial > urweb

comparison lib/ur/top.ur @ 1434:44f78d6fec29

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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) =