equal
deleted
inserted
replaced
32 instances of its declared type @{typ"'a \<Rightarrow> 'a"} --- this merely suppresses |
32 instances of its declared type @{typ"'a \<Rightarrow> 'a"} --- this merely suppresses |
33 warnings to that effect. |
33 warnings to that effect. |
34 |
34 |
35 However, there is nothing to prevent the user from forming terms such as |
35 However, there is nothing to prevent the user from forming terms such as |
36 @{text"inverse []"} and proving theorems such as @{text"inverse [] |
36 @{text"inverse []"} and proving theorems such as @{text"inverse [] |
37 = inverse []"}, although we never defined inverse on lists. We hasten to say |
37 = inverse []"} when inverse is not defined on lists. Proving theorems about |
38 that there is nothing wrong with such terms and theorems. But it would be |
38 undefined constants does not endanger soundness, but it is pointless. |
39 nice if we could prevent their formation, simply because it is very likely |
39 To prevent such terms from even being formed requires the use of type classes. |
40 that the user did not mean to write what he did. Thus she had better not waste |
|
41 her time pursuing it further. This requires the use of type classes. |
|
42 *} |
40 *} |
43 (*<*)end(*>*) |
41 (*<*)end(*>*) |