diff lib/top.urs @ 329:eec65c11d3e2

foldTR2
author Adam Chlipala <adamc@hcoop.net>
date Sat, 13 Sep 2008 10:30:45 -0400
parents e457d8972ff1
children 02d15d81ae9b
line wrap: on
line diff
--- a/lib/top.urs	Thu Sep 11 19:59:31 2008 -0400
+++ b/lib/top.urs	Sat Sep 13 10:30:45 2008 -0400
@@ -1,3 +1,6 @@
+con idT = fn t :: Type => t
+con record = fn t :: {Type} => $t
+
 con mapTT = fn f :: Type -> Type => fold (fn nm t acc => [nm] ~ acc =>
         [nm = f t] ++ acc) []
 
@@ -6,3 +9,8 @@
 
 val txt : t ::: Type -> ctx ::: {Unit} -> use ::: {Type} -> show t -> t
         -> xml ctx use []
+
+val foldTR2 : tf1 :: (Type -> Type) -> tf2 :: (Type -> Type) -> tr :: ({Type} -> Type)
+        -> (nm :: Name -> t :: Type -> rest :: {Type} -> [nm] ~ rest
+                -> tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
+        -> tr [] -> r :: {Type} -> $(mapTT tf1 r) -> $(mapTT tf2 r) -> tr r