Mercurial > urweb

comparison lib/ur/top.urs @ 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 8631e9ed0ee8
children aa0c6382aa57
comparison
equal deleted inserted replaced
1433:66092ce45a76 1434:44f78d6fec29
29 con snd3 = K1 ==> K2 ==> K3 ==> fn t :: (K1 * K2 * K3) => t.2 29 con snd3 = K1 ==> K2 ==> K3 ==> fn t :: (K1 * K2 * K3) => t.2
30 con thd3 = K1 ==> K2 ==> K3 ==> fn t :: (K1 * K2 * K3) => t.3 30 con thd3 = K1 ==> K2 ==> K3 ==> fn t :: (K1 * K2 * K3) => t.3
31 31
32 con mapU = K ==> fn f :: K => map (fn _ :: Unit => f) 32 con mapU = K ==> fn f :: K => map (fn _ :: Unit => f)
33 33
34 con ex = fn tf :: (Type -> Type) => 34 con ex :: K --> (K -> Type) -> Type
35 res ::: Type -> (choice :: Type -> tf choice -> res) -> res 35
36 36 val ex_intro : K --> tf :: (K -> Type) -> choice :: K -> tf choice -> ex tf
37 val ex : tf :: (Type -> Type) -> choice :: Type -> tf choice -> ex tf 37 val ex_elim : K --> tf ::: (K -> Type) -> ex tf -> res ::: Type -> (choice :: K -> tf choice -> res) -> res
38 38
39 val compose : t1 ::: Type -> t2 ::: Type -> t3 ::: Type 39 val compose : t1 ::: Type -> t2 ::: Type -> t3 ::: Type
40 -> (t2 -> t3) -> (t1 -> t2) -> (t1 -> t3) 40 -> (t2 -> t3) -> (t1 -> t2) -> (t1 -> t3)
41 41
42 val show_option : t ::: Type -> show t -> show (option t) 42 val show_option : t ::: Type -> show t -> show (option t)