diff options
author | Adam Chlipala <adam@chlipala.net> | 2012-05-19 11:32:12 -0400 |
---|---|---|
committer | Adam Chlipala <adam@chlipala.net> | 2012-05-19 11:32:12 -0400 |
commit | a4bcc72f9e763e49b3ffefff09b1fe8924e440e1 (patch) | |
tree | 04d2d95798a412261154293e71323e4069718bf6 /lib/ur/list.ur | |
parent | 2be1e51f8036b1b473553d16f11ca63b068146ad (diff) |
Some standard library additions from Edward Z. Yang
Diffstat (limited to 'lib/ur/list.ur')
-rw-r--r-- | lib/ur/list.ur | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/lib/ur/list.ur b/lib/ur/list.ur index 2d5addc9..bce5335e 100644 --- a/lib/ur/list.ur +++ b/lib/ur/list.ur @@ -424,3 +424,16 @@ fun drop [a] (n : int) (xs : list a) : list a = fun splitAt [a] (n : int) (xs : list a) : list a * list a = (take n xs, drop n xs) + +fun mapXiM [m ::: Type -> Type] (_ : monad m) [a] [ctx ::: {Unit}] (f : int -> a -> m (xml ctx [] [])) : t a -> m (xml ctx [] []) = + let + fun mapXiM' i ls = + case ls of + [] => return <xml/> + | x :: ls => + this <- f i x; + rest <- mapXiM' (i+1) ls; + return <xml>{this}{rest}</xml> + in + mapXiM' 0 + end |