Mercurial > urweb
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 |