Mercurial > urweb
diff 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 |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/lib/ur/list.ur Thu May 14 08:13:54 2009 -0400 @@ -0,0 +1,31 @@ +datatype t = datatype Basis.list + +val show (a ::: Type) (_ : show a) = + let + fun show' (ls : list a) = + case ls of + [] => "[]" + | x :: ls => show x ^ " :: " ^ show' ls + in + mkShow show' + end + +val rev (a ::: Type) = + let + fun rev' acc (ls : list a) = + case ls of + [] => acc + | x :: ls => rev' (x :: acc) ls + in + rev' [] + end + +fun mp (a ::: Type) (b ::: Type) f = + let + fun mp' acc ls = + case ls of + [] => rev acc + | x :: ls => mp' (f x :: acc) ls + in + mp' [] + end