Mercurial > urweb
comparison lib/ur/list.ur @ 794:dc3fc3f3b834
Improving/reordering Unpoly and Especialize; pathmaps
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Thu, 14 May 2009 08:13:54 -0400 |
| parents | |
| children | 6271f0e3c272 |
comparison
equal
deleted
inserted
replaced
| 793:3e5d1c6ae30c | 794:dc3fc3f3b834 |
|---|---|
| 1 datatype t = datatype Basis.list | |
| 2 | |
| 3 val show (a ::: Type) (_ : show a) = | |
| 4 let | |
| 5 fun show' (ls : list a) = | |
| 6 case ls of | |
| 7 [] => "[]" | |
| 8 | x :: ls => show x ^ " :: " ^ show' ls | |
| 9 in | |
| 10 mkShow show' | |
| 11 end | |
| 12 | |
| 13 val rev (a ::: Type) = | |
| 14 let | |
| 15 fun rev' acc (ls : list a) = | |
| 16 case ls of | |
| 17 [] => acc | |
| 18 | x :: ls => rev' (x :: acc) ls | |
| 19 in | |
| 20 rev' [] | |
| 21 end | |
| 22 | |
| 23 fun mp (a ::: Type) (b ::: Type) f = | |
| 24 let | |
| 25 fun mp' acc ls = | |
| 26 case ls of | |
| 27 [] => rev acc | |
| 28 | x :: ls => mp' (f x :: acc) ls | |
| 29 in | |
| 30 mp' [] | |
| 31 end |