equal
deleted
inserted
replaced
35 the definitions do intentionally define \isa{inverse} only at |
35 the definitions do intentionally define \isa{inverse} only at |
36 instances of its declared type \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} --- this merely suppresses |
36 instances of its declared type \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} --- this merely suppresses |
37 warnings to that effect. |
37 warnings to that effect. |
38 |
38 |
39 However, there is nothing to prevent the user from forming terms such as |
39 However, there is nothing to prevent the user from forming terms such as |
40 \isa{inverse\ {\isacharbrackleft}{\isacharbrackright}} and proving theorems such as \isa{inverse\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ inverse\ {\isacharbrackleft}{\isacharbrackright}}, although we never defined inverse on lists. We hasten to say |
40 \isa{inverse\ {\isacharbrackleft}{\isacharbrackright}} and proving theorems such as \isa{inverse\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ inverse\ {\isacharbrackleft}{\isacharbrackright}} when inverse is not defined on lists. Proving theorems about |
41 that there is nothing wrong with such terms and theorems. But it would be |
41 undefined constants does not endanger soundness, but it is pointless. |
42 nice if we could prevent their formation, simply because it is very likely |
42 To prevent such terms from even being formed requires the use of type classes.% |
43 that the user did not mean to write what he did. Thus she had better not waste |
|
44 her time pursuing it further. This requires the use of type classes.% |
|
45 \end{isamarkuptext}% |
43 \end{isamarkuptext}% |
46 \end{isabellebody}% |
44 \end{isabellebody}% |
47 %%% Local Variables: |
45 %%% Local Variables: |
48 %%% mode: latex |
46 %%% mode: latex |
49 %%% TeX-master: "root" |
47 %%% TeX-master: "root" |