equal
deleted
inserted
replaced
3 begin |
3 begin |
4 |
4 |
5 datatype 'a list = Nil ("[]") |
5 datatype 'a list = Nil ("[]") |
6 | Cons 'a "'a list" (infixr "#" 65) |
6 | Cons 'a "'a list" (infixr "#" 65) |
7 |
7 |
8 consts app :: "'a list => 'a list => 'a list" (infixr "@" 65) |
8 primrec app :: "'a list => 'a list => 'a list" (infixr "@" 65) |
9 rev :: "'a list => 'a list" |
9 where |
10 |
10 "[] @ ys = ys" | |
11 primrec |
|
12 "[] @ ys = ys" |
|
13 "(x # xs) @ ys = x # (xs @ ys)" |
11 "(x # xs) @ ys = x # (xs @ ys)" |
14 |
12 |
15 primrec |
13 primrec rev :: "'a list => 'a list" where |
16 "rev [] = []" |
14 "rev [] = []" | |
17 "rev (x # xs) = (rev xs) @ (x # [])" |
15 "rev (x # xs) = (rev xs) @ (x # [])" |