Ur/Web: lib/ur/list.ur annotate

Improving/reordering Unpoly and Especialize; pathmaps

author	Adam Chlipala <adamc@hcoop.net>
date	Thu, 14 May 2009 08:13:54 -0400
parents
children	6271f0e3c272

rev	line source
adamc@794	1 datatype t = datatype Basis.list
adamc@794	2
adamc@794	3 val show (a ::: Type) (_ : show a) =
adamc@794	4 let
adamc@794	5 fun show' (ls : list a) =
adamc@794	6 case ls of
adamc@794	7 [] => "[]"
adamc@794	8 \| x :: ls => show x ^ " :: " ^ show' ls
adamc@794	9 in
adamc@794	10 mkShow show'
adamc@794	11 end
adamc@794	12
adamc@794	13 val rev (a ::: Type) =
adamc@794	14 let
adamc@794	15 fun rev' acc (ls : list a) =
adamc@794	16 case ls of
adamc@794	17 [] => acc
adamc@794	18 \| x :: ls => rev' (x :: acc) ls
adamc@794	19 in
adamc@794	20 rev' []
adamc@794	21 end
adamc@794	22
adamc@794	23 fun mp (a ::: Type) (b ::: Type) f =
adamc@794	24 let
adamc@794	25 fun mp' acc ls =
adamc@794	26 case ls of
adamc@794	27 [] => rev acc
adamc@794	28 \| x :: ls => mp' (f x :: acc) ls
adamc@794	29 in
adamc@794	30 mp' []
adamc@794	31 end

Mercurial > urweb