diff lib/ur/top.urs @ 910:8e540df3294d

grid1 compiles but gets stuck in JS
author Adam Chlipala <adamc@hcoop.net>
date Tue, 25 Aug 2009 13:57:56 -0400
parents 7a4b026e45dd
children 37dd42935dad
line wrap: on
line diff
--- a/lib/ur/top.urs	Sat Aug 22 16:32:31 2009 -0400
+++ b/lib/ur/top.urs	Tue Aug 25 13:57:56 2009 -0400
@@ -84,6 +84,14 @@
              -> tr []
              -> r :: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> tr r
 
+val foldR3 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type)
+             -> tr :: ({K} -> Type)
+             -> (nm :: Name -> t :: K -> rest :: {K}
+                 -> [[nm] ~ rest] =>
+                       tf1 t -> tf2 t -> tf3 t -> tr rest -> tr ([nm = t] ++ rest))
+             -> 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] =>
@@ -97,6 +105,13 @@
               -> r :: {K} -> folder r
               -> $(map tf1 r) -> $(map tf2 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 queryI : tables ::: {{Type}} -> exps ::: {Type}
              -> [tables ~ exps] =>
              sql_query tables exps