summaryrefslogtreecommitdiff
path: root/lib/ur/list.urs
diff options
context:
space:
mode:
authorGravatar Benjamin Barenblat <bbaren@mit.edu>2018-06-17 09:12:52 -0400
committerGravatar Benjamin Barenblat <bbaren@mit.edu>2018-06-17 09:12:52 -0400
commit095c2640aa2070ed4e2765875238d5e6e6673856 (patch)
tree9306beb3fef29a99d9436dc00e2d8c57fb3e0c7b /lib/ur/list.urs
parent8c58ba2e1db6e97ca1f18fd9ca52ffead53e4a4f (diff)
parent34eb9eba9a724433f9c37c39cf43e9e10cf55220 (diff)
Merge branch 'upstream' into dfsg_clean20180616+dfsg
Diffstat (limited to 'lib/ur/list.urs')
-rw-r--r--lib/ur/list.urs4
1 files changed, 4 insertions, 0 deletions
diff --git a/lib/ur/list.urs b/lib/ur/list.urs
index fd56679d..fe730152 100644
--- a/lib/ur/list.urs
+++ b/lib/ur/list.urs
@@ -42,6 +42,8 @@ val filter : a ::: Type -> (a -> bool) -> t a -> t a
val exists : a ::: Type -> (a -> bool) -> t a -> bool
+val existsM : m ::: (Type -> Type) -> monad m -> a ::: Type -> (a -> m bool) -> t a -> m bool
+
val foldlM : m ::: (Type -> Type) -> monad m -> a ::: Type -> b ::: Type
-> (a -> b -> m b) -> b -> t a -> m b
@@ -58,6 +60,8 @@ val mem : a ::: Type -> eq a -> a -> t a -> bool
val find : a ::: Type -> (a -> bool) -> t a -> option a
+val findM : m ::: (Type -> Type) -> monad m -> a ::: Type -> (a -> m bool) -> t a -> m (option a)
+
val search : a ::: Type -> b ::: Type -> (a -> option b) -> t a -> option b
val all : a ::: Type -> (a -> bool) -> t a -> bool