summaryrefslogtreecommitdiff
path: root/lib/ur/list.ur
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-05-30 14:44:29 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-05-30 14:44:29 -0400
commitbd0d3db78996b00e153252f03b02551ac3fde4cf (patch)
tree0fad0449847add724cfee07969e95597f7136ea8 /lib/ur/list.ur
parent54276f5a38163eb7997c574810faed0cc6dea35c (diff)
Defer pattern-matching exhaustiveness checks and normalize pattern types more thoroughly
Diffstat (limited to 'lib/ur/list.ur')
-rw-r--r--lib/ur/list.ur13
1 files changed, 13 insertions, 0 deletions
diff --git a/lib/ur/list.ur b/lib/ur/list.ur
index 8493f2f5..0776ff30 100644
--- a/lib/ur/list.ur
+++ b/lib/ur/list.ur
@@ -74,6 +74,19 @@ fun mapM [m ::: (Type -> Type)] (_ : monad m) [a] [b] f =
mapM' []
end
+fun mapXM [m ::: (Type -> Type)] (_ : monad m) [a] [ctx ::: {Unit}] f =
+ let
+ fun mapXM' ls =
+ case ls of
+ [] => return <xml/>
+ | x :: ls =>
+ this <- f x;
+ rest <- mapXM' ls;
+ return <xml>{this}{rest}</xml>
+ in
+ mapXM'
+ end
+
fun filter [a] f =
let
fun fil acc ls =