| changeset 48966 | 6e15de7dd871 |
| parent 48965 | 1fead823c7c6 |
| child 48967 | 389e44f9e47a |
| 48965:1fead823c7c6 | 48966:6e15de7dd871 |
|---|---|
1 theory ToyList |
|
2 imports Datatype |
|
3 begin |
|
4 |
|
5 datatype 'a list = Nil ("[]") |
|
6 | Cons 'a "'a list" (infixr "#" 65) |
|
7 |
|
8 (* This is the append function: *) |
|
9 primrec app :: "'a list => 'a list => 'a list" (infixr "@" 65) |
|
10 where |
|
11 "[] @ ys = ys" | |
|
12 "(x # xs) @ ys = x # (xs @ ys)" |
|
13 |
|
14 primrec rev :: "'a list => 'a list" where |
|
15 "rev [] = []" | |
|
16 "rev (x # xs) = (rev xs) @ (x # [])" |