Mercurial > urweb
comparison 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 |
comparison
equal
deleted
inserted
replaced
| 1766:92cfc69419bd | 1768:a613cae954ca |
|---|---|
| 422 [] => [] | 422 [] => [] |
| 423 | x :: xs => drop (n-1) xs | 423 | x :: xs => drop (n-1) xs |
| 424 | 424 |
| 425 fun splitAt [a] (n : int) (xs : list a) : list a * list a = | 425 fun splitAt [a] (n : int) (xs : list a) : list a * list a = |
| 426 (take n xs, drop n xs) | 426 (take n xs, drop n xs) |
| 427 | |
| 428 fun mapXiM [m ::: Type -> Type] (_ : monad m) [a] [ctx ::: {Unit}] (f : int -> a -> m (xml ctx [] [])) : t a -> m (xml ctx [] []) = | |
| 429 let | |
| 430 fun mapXiM' i ls = | |
| 431 case ls of | |
| 432 [] => return <xml/> | |
| 433 | x :: ls => | |
| 434 this <- f i x; | |
| 435 rest <- mapXiM' (i+1) ls; | |
| 436 return <xml>{this}{rest}</xml> | |
| 437 in | |
| 438 mapXiM' 0 | |
| 439 end |