Ur/Web: demo/list.ur annotate

Fix a subtle renaming problem in elaborating functor applications

author	Adam Chlipala <adam@chlipala.net>
date	Fri, 14 Feb 2014 15:11:22 -0500
parents	669ac5e9a69e
children

rev	line source
adamc@397	1 datatype list t = Nil \| Cons of t * list t
adamc@397	2
adamc@823	3 fun length [t] (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@823	13 fun rev [t] (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