diff options
author | Adam Chlipala <adamc@hcoop.net> | 2009-07-19 17:45:02 -0400 |
---|---|---|
committer | Adam Chlipala <adamc@hcoop.net> | 2009-07-19 17:45:02 -0400 |
commit | 94a1373401529f500640b0c0628e7173612cdabe (patch) | |
tree | 89ce0f6149e50fdfece4b083c2be2033c7727c63 /lib/ur/top.urs | |
parent | 19cd9e965929d541e6714f62154f01b9e487a712 (diff) |
Working on Grid; have gone from one dynamic table bizareness to another
Diffstat (limited to 'lib/ur/top.urs')
-rw-r--r-- | lib/ur/top.urs | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/lib/ur/top.urs b/lib/ur/top.urs index 4ed64075..33c90651 100644 --- a/lib/ur/top.urs +++ b/lib/ur/top.urs @@ -21,7 +21,7 @@ end val not : bool -> bool -con idT = fn t :: Type => t +con id = K ==> fn t :: K => t con record = fn t :: {Type} => $t con fst = K1 ==> K2 ==> fn t :: (K1 * K2) => t.1 con snd = K1 ==> K2 ==> fn t :: (K1 * K2) => t.2 @@ -45,6 +45,13 @@ val read_option : t ::: Type -> read t -> read (option t) val txt : t ::: Type -> ctx ::: {Unit} -> use ::: {Type} -> show t -> t -> xml ctx use [] +val mp : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) + -> (t ::: K -> tf1 t -> tf2 t) + -> r :: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) +val map2 : K1 --> K2 --> tf1 :: (K1 -> Type) -> tf2 :: (K2 -> Type) -> tf :: (K1 -> K2) + -> (t ::: K1 -> tf1 t -> tf2 (tf t)) + -> r :: {K1} -> folder r -> $(map tf1 r) -> $(map tf2 (map tf r)) + val foldUR : tf :: Type -> tr :: ({Unit} -> Type) -> (nm :: Name -> rest :: {Unit} -> [[nm] ~ rest] => |