changeset 56420 | b266e7a86485 |
parent 48985 | 5386df44a037 |
56419:f47de9e82b0f | 56420:b266e7a86485 |
---|---|
1 theory MyList |
|
2 imports Main |
|
3 begin |
|
4 |
|
5 datatype 'a list = Nil | Cons 'a "'a list" |
|
6 |
|
7 fun app :: "'a list => 'a list => 'a list" where |
|
8 "app Nil ys = ys" | |
|
9 "app (Cons x xs) ys = Cons x (app xs ys)" |
|
10 |
|
11 fun rev :: "'a list => 'a list" where |
|
12 "rev Nil = Nil" | |
|
13 "rev (Cons x xs) = app (rev xs) (Cons x Nil)" |
|
14 |
|
15 value "rev(Cons True (Cons False Nil))" |
|
16 |
|
17 end |