diff lib/ur/list.urs @ 800:e92cfac1608f

Proper lifting of MonoEnv stored expressions; avoidance of onchange clobbering
author Adam Chlipala <adamc@hcoop.net>
date Thu, 14 May 2009 13:18:31 -0400
parents 6271f0e3c272
children 395a5d450cc0
line wrap: on
line diff
--- a/lib/ur/list.urs	Thu May 14 11:04:56 2009 -0400
+++ b/lib/ur/list.urs	Thu May 14 13:18:31 2009 -0400
@@ -7,3 +7,6 @@
 val mp : a ::: Type -> b ::: Type -> (a -> b) -> t a -> t b
 
 val mapX : a ::: Type -> ctx ::: {Unit} -> (a -> xml ctx [] []) -> t a -> xml ctx [] []
+
+val mapM : m ::: (Type -> Type) -> monad m -> a ::: Type -> b ::: Type
+           -> (a -> m b) -> list a -> m (list b)