Ur/Web: demo/list.ur annotate

Injected an enumeration

author	Adam Chlipala <adamc@hcoop.net>
date	Thu, 08 Jan 2009 09:57:45 -0500
parents	7ef4b2911b09
children	669ac5e9a69e

rev	line source
adamc@397	1 datatype list t = Nil \| Cons of t * list t
adamc@397	2
adamc@501	3 fun length (t ::: Type) (ls : list t) =
adamc@501	4 let
adamc@501	5 fun length' (ls : list t) (acc : int) =
adamc@501	6 case ls of
adamc@501	7 Nil => acc
adamc@501	8 \| Cons (_, ls') => length' ls' (acc + 1)
adamc@501	9 in
adamc@501	10 length' ls 0
adamc@501	11 end
adamc@397	12
adamc@501	13 fun rev (t ::: Type) (ls : list t) =
adamc@501	14 let
adamc@501	15 fun rev' (ls : list t) (acc : list t) =
adamc@501	16 case ls of
adamc@501	17 Nil => acc
adamc@501	18 \| Cons (x, ls') => rev' ls' (Cons (x, acc))
adamc@501	19 in
adamc@501	20 rev' ls Nil
adamc@501	21 end

Mercurial > urweb