author | wenzelm |
Tue, 09 May 2000 15:10:25 +0200 | |
changeset 8845 | 03a2ae3059da |
parent 8751 | 9ed0548177fb |
child 8846 | c7d945398677 |
permissions | -rw-r--r-- |
8751 | 1 |
theory ToyList = PreList: |
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 # [])"; |