Ur/Web: demo/list.ur annotate

More ThreadedBlog progress

author	Adam Chlipala <adamc@hcoop.net>
date	Tue, 11 Nov 2008 16:27:51 -0500
parents	4d519baf357c
children	7ef4b2911b09

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

Mercurial > urweb