equal
deleted
inserted
replaced
|
1 % |
|
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{Overloading{\isadigit{2}}}% |
|
4 % |
|
5 \begin{isamarkuptext}% |
|
6 Of course this is not the only possible definition of the two relations. |
|
7 Componentwise% |
|
8 \end{isamarkuptext}% |
|
9 \isacommand{instance}\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}ordrel{\isacharparenright}ordrel\isanewline |
|
10 \isacommand{by}\ intro{\isacharunderscore}classes\isanewline |
|
11 \isanewline |
|
12 \isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline |
|
13 le{\isacharunderscore}list{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}xs\ {\isacharless}{\isacharless}{\isacharequal}\ {\isacharparenleft}ys{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel\ list{\isacharparenright}\ {\isasymequiv}\isanewline |
|
14 \ \ \ \ \ \ \ \ \ \ \ \ \ \ size\ xs\ {\isacharequal}\ size\ ys\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isacharless}size\ xs{\isachardot}\ xs{\isacharbang}i\ {\isacharless}{\isacharless}{\isacharequal}\ ys{\isacharbang}i{\isacharparenright}{\isachardoublequote}% |
|
15 \begin{isamarkuptext}% |
|
16 %However, we retract the componetwise comparison of lists and return |
|
17 |
|
18 Note: only one definition because based on name.% |
|
19 \end{isamarkuptext}% |
|
20 \isanewline |
|
21 \end{isabellebody}% |
|
22 %%% Local Variables: |
|
23 %%% mode: latex |
|
24 %%% TeX-master: "root" |
|
25 %%% End: |