Mercurial > urweb
diff lib/ur/top.urs @ 1172:ad15700272f6
Changing foldRX to mapX
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sun, 28 Feb 2010 13:06:10 -0500 |
parents | 7fc4e0087e50 |
children | 983d9b38abc7 |
line wrap: on
line diff
--- a/lib/ur/top.urs Sat Feb 27 16:49:11 2010 -0500 +++ b/lib/ur/top.urs Sun Feb 28 13:06:10 2010 -0500 @@ -98,25 +98,30 @@ -> tr [] -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> tr r -val foldRX : K --> tf :: (K -> Type) -> ctx :: {Unit} - -> (nm :: Name -> t :: K -> rest :: {K} - -> [[nm] ~ rest] => - tf t -> xml ctx [] []) - -> r ::: {K} -> folder r -> $(map tf r) -> xml ctx [] [] +val mapUX : tf :: Type -> ctx :: {Unit} + -> (nm :: Name -> rest :: {Unit} -> [[nm] ~ rest] => + tf -> xml ctx [] []) + -> r ::: {Unit} -> folder r -> $(mapU tf r) -> xml ctx [] [] -val foldRX2 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> ctx :: {Unit} - -> (nm :: Name -> t :: K -> rest :: {K} - -> [[nm] ~ rest] => - tf1 t -> tf2 t -> xml ctx [] []) - -> r ::: {K} -> folder r - -> $(map tf1 r) -> $(map tf2 r) -> xml ctx [] [] +val mapX : K --> tf :: (K -> Type) -> ctx :: {Unit} + -> (nm :: Name -> t :: K -> rest :: {K} + -> [[nm] ~ rest] => + tf t -> xml ctx [] []) + -> r ::: {K} -> folder r -> $(map tf r) -> xml ctx [] [] -val foldRX3 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type) -> ctx :: {Unit} - -> (nm :: Name -> t :: K -> rest :: {K} - -> [[nm] ~ rest] => - tf1 t -> tf2 t -> tf3 t -> xml ctx [] []) - -> r ::: {K} -> folder r - -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> xml ctx [] [] +val mapX2 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> ctx :: {Unit} + -> (nm :: Name -> t :: K -> rest :: {K} + -> [[nm] ~ rest] => + tf1 t -> tf2 t -> xml ctx [] []) + -> r ::: {K} -> folder r + -> $(map tf1 r) -> $(map tf2 r) -> xml ctx [] [] + +val mapX3 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type) -> ctx :: {Unit} + -> (nm :: Name -> t :: K -> rest :: {K} + -> [[nm] ~ rest] => + tf1 t -> tf2 t -> tf3 t -> xml ctx [] []) + -> r ::: {K} -> folder r + -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> xml ctx [] [] val queryL : tables ::: {{Type}} -> exps ::: {Type} -> [tables ~ exps] =>