aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/ur/list.ur
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2018-08-25 18:26:33 -0400
committerGravatar Adam Chlipala <adam@chlipala.net>2018-08-25 18:26:33 -0400
commit7eec6f5c0d702323bd735e2184ff74f27ad37d17 (patch)
treecc74a9a1a9add8b8caf48d6574f40180db99c3c9 /lib/ur/list.ur
parent0e41b2ab9485f46c4303be46d41e39203eeb7138 (diff)
List.allM
Diffstat (limited to 'lib/ur/list.ur')
-rw-r--r--lib/ur/list.ur17
1 files changed, 16 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 =