Mercurial > urweb
diff lib/ur/list.ur @ 1768:a613cae954ca
Some standard library additions from Edward Z. Yang
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Sat, 19 May 2012 11:32:12 -0400 |
parents | f4cb4eebf7ae |
children | 146ec8e90063 |
line wrap: on
line diff
--- a/lib/ur/list.ur Thu May 17 10:20:24 2012 -0400 +++ b/lib/ur/list.ur Sat May 19 11:32:12 2012 -0400 @@ -424,3 +424,16 @@ 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