diff lib/ur/top.urs @ 993:10114d7b7477

SELECT DISTINCT; eta expansion during Cjrization
author Adam Chlipala <adamc@hcoop.net>
date Tue, 06 Oct 2009 15:39:27 -0400
parents 37dd42935dad
children 61c30f0742d7
line wrap: on
line diff
--- a/lib/ur/top.urs	Tue Oct 06 13:11:03 2009 -0400
+++ b/lib/ur/top.urs	Tue Oct 06 15:39:27 2009 -0400
@@ -45,6 +45,9 @@
 val txt : t ::: Type -> ctx ::: {Unit} -> use ::: {Type} -> show t -> t
           -> xml ctx use []
 
+val map0 : K --> tf :: (K -> Type)
+           -> (t :: K -> tf t)
+           -> r :: {K} -> folder r -> $(map tf r)
 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)