equal
deleted
inserted
replaced
1 (*<*)theory Overloading2 = Overloading1:(*>*) |
1 (*<*)theory Overloading2 = Overloading1:(*>*) |
2 |
2 |
3 text{* |
3 text{* |
4 Of course this is not the only possible definition of the two relations. |
4 Of course this is not the only possible definition of the two relations. |
5 Componentwise |
5 Componentwise comparison of lists of equal length also makes sense. This time |
|
6 the elements of the list must also be of class @{text ordrel} to permit their |
|
7 comparison: |
6 *} |
8 *} |
7 |
9 |
8 instance list :: (ordrel)ordrel |
10 instance list :: (ordrel)ordrel |
9 by intro_classes |
11 by intro_classes |
10 |
12 |
11 defs (overloaded) |
13 defs (overloaded) |
12 le_list_def: "xs <<= (ys::'a::ordrel list) \<equiv> |
14 le_list_def: "xs <<= (ys::'a::ordrel list) \<equiv> |
13 size xs = size ys \<and> (\<forall>i<size xs. xs!i <<= ys!i)" |
15 size xs = size ys \<and> (\<forall>i<size xs. xs!i <<= ys!i)" |
14 |
16 |
15 text{* |
17 text{*\noindent |
|
18 The infix function @{text"!"} yields the nth element of a list. |
16 %However, we retract the componetwise comparison of lists and return |
19 %However, we retract the componetwise comparison of lists and return |
17 |
20 %Note: only one definition because based on name. |
18 Note: only one definition because based on name. |
21 *}(*<*)end(*>*) |
19 *} |
|
20 (*<*)end(*>*) |
|
21 |
|