| author | wenzelm |
| Sat, 27 Oct 2001 00:00:05 +0200 | |
| changeset 11954 | 3d1780208bf3 |
| parent 5377 | efb799c5ed3c |
| permissions | -rw-r--r-- |
| 5377 | 1 |
ToyList = Datatype + |
2 |
||
3 |
datatype 'a list = Nil ("[]")
|
|
4 |
| Cons 'a ('a list) (infixr "#" 65)
|
|
5 |
||
6 |
consts app :: 'a list => 'a list => 'a list (infixr "@" 65) |
|
7 |
rev :: 'a list => 'a list |
|
8 |
||
9 |
primrec |
|
10 |
"[] @ ys = ys" |
|
11 |
"(x # xs) @ ys = x # (xs @ ys)" |
|
12 |
||
13 |
primrec |
|
14 |
"rev [] = []" |
|
15 |
"rev (x # xs) = (rev xs) @ (x # [])" |
|
16 |
||
17 |
end |