comparison demo/list.ur @ 501:7ef4b2911b09

Some demo improvements
author Adam Chlipala <adamc@hcoop.net>
date Thu, 20 Nov 2008 11:34:36 -0500
parents 4d519baf357c
children 669ac5e9a69e
comparison
equal deleted inserted replaced
500:581554f8e642 501:7ef4b2911b09
1 datatype list t = Nil | Cons of t * list t 1 datatype list t = Nil | Cons of t * list t
2 2
3 fun length' (t ::: Type) (ls : list t) (acc : int) = 3 fun length (t ::: Type) (ls : list t) =
4 case ls of 4 let
5 Nil => acc 5 fun length' (ls : list t) (acc : int) =
6 | Cons (_, ls') => length' ls' (acc + 1) 6 case ls of
7 Nil => acc
8 | Cons (_, ls') => length' ls' (acc + 1)
9 in
10 length' ls 0
11 end
7 12
8 fun length (t ::: Type) (ls : list t) = length' ls 0 13 fun rev (t ::: Type) (ls : list t) =
9 14 let
10 fun rev' (t ::: Type) (ls : list t) (acc : list t) = 15 fun rev' (ls : list t) (acc : list t) =
11 case ls of 16 case ls of
12 Nil => acc 17 Nil => acc
13 | Cons (x, ls') => rev' ls' (Cons (x, acc)) 18 | Cons (x, ls') => rev' ls' (Cons (x, acc))
14 19 in
15 fun rev (t ::: Type) (ls : list t) = rev' ls Nil 20 rev' ls Nil
21 end