equal
deleted
inserted
replaced
|
1 % |
|
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{Overloading}% |
|
4 \isacommand{instance}\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}{\isachardoublequote}term{\isachardoublequote}{\isacharparenright}ordrel\isanewline |
|
5 \isacommand{by}\ intro{\isacharunderscore}classes% |
|
6 \begin{isamarkuptext}% |
|
7 \noindent |
|
8 This means. Of course we should also define the meaning of \isa{{\isacharless}{\isacharless}{\isacharequal}} and |
|
9 \isa{{\isacharless}{\isacharless}} on lists.% |
|
10 \end{isamarkuptext}% |
|
11 \isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline |
|
12 prefix{\isacharunderscore}def{\isacharcolon}\isanewline |
|
13 \ \ {\isachardoublequote}xs\ {\isacharless}{\isacharless}{\isacharequal}\ {\isacharparenleft}ys{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel\ list{\isacharparenright}\ \ {\isasymequiv}\ \ {\isasymexists}zs{\isachardot}\ ys\ {\isacharequal}\ xs{\isacharat}zs{\isachardoublequote}\isanewline |
|
14 strict{\isacharunderscore}prefix{\isacharunderscore}def{\isacharcolon}\isanewline |
|
15 \ \ {\isachardoublequote}xs\ {\isacharless}{\isacharless}\ {\isacharparenleft}ys{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel\ list{\isacharparenright}\ \ \ {\isasymequiv}\ \ xs\ {\isacharless}{\isacharless}{\isacharequal}\ ys\ {\isasymand}\ xs\ {\isasymnoteq}\ ys{\isachardoublequote}% |
|
16 \begin{isamarkuptext}% |
|
17 We could also have made the second definition non-overloaded once and for |
|
18 all: \isa{x\ {\isacharless}{\isacharless}\ y\ {\isasymequiv}\ x\ {\isacharless}{\isacharless}{\isacharequal}\ y\ {\isasymand}\ x\ {\isasymnoteq}\ y}. This would have saved us writing |
|
19 many similar definitions at different types, but it would also have fixed |
|
20 that \isa{{\isacharless}{\isacharless}} is defined in terms of \isa{{\isacharless}{\isacharless}{\isacharequal}} and never the other way |
|
21 around. Below you will see why we want to avoid this asymmetry.% |
|
22 \end{isamarkuptext}% |
|
23 \end{isabellebody}% |
|
24 %%% Local Variables: |
|
25 %%% mode: latex |
|
26 %%% TeX-master: "root" |
|
27 %%% End: |