Mercurial > urweb

comparison lib/ur/top.urs @ 898:d1d0b18afd3d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Working on Grid; have gone from one dynamic table bizareness to another
author Adam Chlipala <adamc@hcoop.net>
date Sun, 19 Jul 2009 17:45:02 -0400
parents 87a7702d681d
children 7a4b026e45dd
comparison
equal deleted inserted replaced
897:2faf558b2d05 898:d1d0b18afd3d
19 end 19 end
20 20
21 21
22 val not : bool -> bool 22 val not : bool -> bool
23 23
24 con idT = fn t :: Type => t 24 con id = K ==> fn t :: K => t
25 con record = fn t :: {Type} => $t 25 con record = fn t :: {Type} => $t
26 con fst = K1 ==> K2 ==> fn t :: (K1 * K2) => t.1 26 con fst = K1 ==> K2 ==> fn t :: (K1 * K2) => t.1
27 con snd = K1 ==> K2 ==> fn t :: (K1 * K2) => t.2 27 con snd = K1 ==> K2 ==> fn t :: (K1 * K2) => t.2
28 con fst3 = K1 ==> K2 ==> K3 ==> fn t :: (K1 * K2 * K3) => t.1 28 con fst3 = K1 ==> K2 ==> K3 ==> fn t :: (K1 * K2 * K3) => t.1
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
42 val show_option : t ::: Type -> show t -> show (option t) 42 val show_option : t ::: Type -> show t -> show (option t)
43 val read_option : t ::: Type -> read t -> read (option t) 43 val read_option : t ::: Type -> read t -> read (option t)
44 44
45 val txt : t ::: Type -> ctx ::: {Unit} -> use ::: {Type} -> show t -> t 45 val txt : t ::: Type -> ctx ::: {Unit} -> use ::: {Type} -> show t -> t
46 -> xml ctx use [] 46 -> xml ctx use []
47
48 val mp : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type)
49 -> (t ::: K -> tf1 t -> tf2 t)
50 -> r :: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r)
51 val map2 : K1 --> K2 --> tf1 :: (K1 -> Type) -> tf2 :: (K2 -> Type) -> tf :: (K1 -> K2)
52 -> (t ::: K1 -> tf1 t -> tf2 (tf t))
53 -> r :: {K1} -> folder r -> $(map tf1 r) -> $(map tf2 (map tf r))
47 54
48 val foldUR : tf :: Type -> tr :: ({Unit} -> Type) 55 val foldUR : tf :: Type -> tr :: ({Unit} -> Type)
49 -> (nm :: Name -> rest :: {Unit} 56 -> (nm :: Name -> rest :: {Unit}
50 -> [[nm] ~ rest] => 57 -> [[nm] ~ rest] =>
51 tf -> tr rest -> tr ([nm] ++ rest)) 58 tf -> tr rest -> tr ([nm] ++ rest))