aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorAdam Chlipala <adam@chlipala.net>2018-08-25 18:26:33 -0400
committerAdam Chlipala <adam@chlipala.net>2018-08-25 18:26:33 -0400
commit7eec6f5c0d702323bd735e2184ff74f27ad37d17 (patch)
treecc74a9a1a9add8b8caf48d6574f40180db99c3c9
parent0e41b2ab9485f46c4303be46d41e39203eeb7138 (diff)
List.allM
-rw-r--r--lib/ur/list.ur17
-rw-r--r--lib/ur/list.urs2
2 files changed, 18 insertions, 1 deletions
diff --git a/lib/ur/list.ur b/lib/ur/list.ur
index 95d6fbc8..d28d2868 100644
--- a/lib/ur/list.ur
+++ b/lib/ur/list.ur
@@ -319,7 +319,7 @@ fun filterM [m] (_ : monad m) [a] (p : a -> m bool) =
filterM' []
end
-fun all [m] f =
+fun all [a] f =
let
fun all' ls =
case ls of
@@ -329,6 +329,21 @@ fun all [m] f =
all'
end
+fun allM [m] (_ : monad m) [a] f =
+ let
+ fun all' ls =
+ case ls of
+ [] => return True
+ | x :: ls =>
+ b <- f x;
+ if b then
+ all' ls
+ else
+ return False
+ in
+ all'
+ end
+
fun app [m] (_ : monad m) [a] f =
let
fun app' ls =
diff --git a/lib/ur/list.urs b/lib/ur/list.urs
index fe730152..f4593dda 100644
--- a/lib/ur/list.urs
+++ b/lib/ur/list.urs
@@ -66,6 +66,8 @@ val search : a ::: Type -> b ::: Type -> (a -> option b) -> t a -> option b
val all : a ::: Type -> (a -> bool) -> t a -> bool
+val allM : m ::: (Type -> Type) -> monad m -> a ::: Type -> (a -> m bool) -> t a -> m bool
+
val app : m ::: (Type -> Type) -> monad m -> a ::: Type
-> (a -> m unit) -> t a -> m unit