summaryrefslogtreecommitdiff
path: root/lib/ur/monad.urs
diff options
context:
space:
mode:
authorGravatar Benjamin Barenblat <bbaren@mit.edu>2015-11-22 10:39:36 -0500
committerGravatar Benjamin Barenblat <bbaren@mit.edu>2015-11-22 10:39:36 -0500
commitbf037ce78c2c76a34ecca0fb8bafa5d5be38968a (patch)
tree3e91b0d0e8e0fb704c7df444283b6c8c63351f95 /lib/ur/monad.urs
parent7d861ea0debf944cb8e3e38d73a8c0197de574b3 (diff)
parent638e838a81e1ccc6594fda1920df441eb21577ae (diff)
Merge branch 'upstream' into dfsg_clean20151122+dfsg
Diffstat (limited to 'lib/ur/monad.urs')
-rw-r--r--lib/ur/monad.urs6
1 files changed, 6 insertions, 0 deletions
diff --git a/lib/ur/monad.urs b/lib/ur/monad.urs
index ce823f4a..8ca8d0a3 100644
--- a/lib/ur/monad.urs
+++ b/lib/ur/monad.urs
@@ -58,6 +58,12 @@ val mapR2 : K --> m ::: (Type -> Type) -> monad m
-> (nm :: Name -> t :: K -> tf1 t -> tf2 t -> m (tr t))
-> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> m ($(map tr r))
+val mapR3 : K --> m ::: (Type -> Type) -> monad m
+ -> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type)
+ -> tr :: (K -> Type)
+ -> (nm :: Name -> t :: K -> tf1 t -> tf2 t -> tf3 t -> m (tr t))
+ -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> m ($(map tr r))
+
val foldMapR : K --> m ::: (Type -> Type) -> monad m
-> tf :: (K -> Type)
-> tf' :: (K -> Type)