author | wenzelm |
Sat, 24 May 2014 20:07:26 +0200 | |
changeset 57083 | 5c26000e1042 |
parent 48985 | src/Doc/Tutorial/ToyList/ToyList1@5386df44a037 |
child 58112 | 8081087096ad |
permissions | -rw-r--r-- |
15136 | 1 |
theory ToyList |
26729 | 2 |
imports Datatype |
15136 | 3 |
begin |
8751 | 4 |
|
5 |
datatype 'a list = Nil ("[]") |
|
9541 | 6 |
| Cons 'a "'a list" (infixr "#" 65) |
8751 | 7 |
|
38430
254a021ed66e
tuned text about "value" and added note on comments.
nipkow
parents:
27015
diff
changeset
|
8 |
(* This is the append function: *) |
27015 | 9 |
primrec app :: "'a list => 'a list => 'a list" (infixr "@" 65) |
10 |
where |
|
11 |
"[] @ ys = ys" | |
|
9541 | 12 |
"(x # xs) @ ys = x # (xs @ ys)" |
8751 | 13 |
|
27015 | 14 |
primrec rev :: "'a list => 'a list" where |
15 |
"rev [] = []" | |
|
9541 | 16 |
"rev (x # xs) = (rev xs) @ (x # [])" |