aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/ur/monad.urs
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2010-02-28 13:06:10 -0500
committerGravatar Adam Chlipala <adamc@hcoop.net>2010-02-28 13:06:10 -0500
commit703c91af7525838dff97f88245bf7482745e771e (patch)
tree514a47d371580960d255dd83a28303a9035c319b /lib/ur/monad.urs
parentf59bbf0b942cd888c798c06ba6841bf94562a438 (diff)
Changing foldRX to mapX
Diffstat (limited to 'lib/ur/monad.urs')
-rw-r--r--lib/ur/monad.urs5
1 files changed, 5 insertions, 0 deletions
diff --git a/lib/ur/monad.urs b/lib/ur/monad.urs
index 698a4b5b..05f201e0 100644
--- a/lib/ur/monad.urs
+++ b/lib/ur/monad.urs
@@ -34,6 +34,11 @@ val foldR3 : K --> m ::: (Type -> Type) -> monad m
-> tr []
-> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> m (tr r)
+val mapR0 : K --> m ::: (Type -> Type) -> monad m
+ -> tr :: (K -> Type)
+ -> (nm :: Name -> t :: K -> m (tr t))
+ -> r ::: {K} -> folder r -> m ($(map tr r))
+
val mapR : K --> m ::: (Type -> Type) -> monad m
-> tf :: (K -> Type)
-> tr :: (K -> Type)