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 | df475a9256347564d3adc1fafc53c4d93b4e73f7 (patch) | |
tree | 04d2d95798a412261154293e71323e4069718bf6 /lib/ur/list.ur | |
parent | 597f9bd0cee0f60fb7dd23d14c6125f5eb6d3f5d (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 |