38 |
38 |
39 On the other hand there are syntactic differences, of course. |
39 On the other hand there are syntactic differences, of course. |
40 Constants \isa{{\isasymodot}} on some type \isa{{\isasymtau}} are rejected by the |
40 Constants \isa{{\isasymodot}} on some type \isa{{\isasymtau}} are rejected by the |
41 type-checker, unless the arity \isa{{\isasymtau}\ {\isasymColon}\ product} is part of the |
41 type-checker, unless the arity \isa{{\isasymtau}\ {\isasymColon}\ product} is part of the |
42 type signature. In our example, this arity may be always added when |
42 type signature. In our example, this arity may be always added when |
43 required by means of an $\INSTANCE$ with the trivial proof |
43 required by means of an $\INSTANCE$ with the default proof $\DDOT$. |
44 $\BY{intro_classes}$. |
|
45 |
44 |
46 \medskip Thus, we may observe the following discipline of using |
45 \medskip Thus, we may observe the following discipline of using |
47 syntactic classes. Overloaded polymorphic constants have their type |
46 syntactic classes. Overloaded polymorphic constants have their type |
48 arguments restricted to an associated (logically trivial) class |
47 arguments restricted to an associated (logically trivial) class |
49 \isa{c}. Only immediately before \emph{specifying} these constants |
48 \isa{c}. Only immediately before \emph{specifying} these constants |
50 on a certain type \isa{{\isasymtau}} do we instantiate \isa{{\isasymtau}\ {\isasymColon}\ c}. |
49 on a certain type \isa{{\isasymtau}} do we instantiate \isa{{\isasymtau}\ {\isasymColon}\ c}. |
51 |
50 |
52 This is done for class \isa{product} and type \isa{bool} as |
51 This is done for class \isa{product} and type \isa{bool} as |
53 follows.% |
52 follows.% |
54 \end{isamarkuptext}% |
53 \end{isamarkuptext}% |
55 \isacommand{instance}\ bool\ {\isacharcolon}{\isacharcolon}\ product\isanewline |
54 \isacommand{instance}\ bool\ {\isacharcolon}{\isacharcolon}\ product\ \isacommand{{\isachardot}{\isachardot}}\isanewline |
56 \ \ \isacommand{by}\ intro{\isacharunderscore}classes\isanewline |
|
57 \isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline |
55 \isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline |
58 \ \ product{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ y\ {\isasymequiv}\ x\ {\isasymand}\ y{\isachardoublequote}% |
56 \ \ product{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ y\ {\isasymequiv}\ x\ {\isasymand}\ y{\isachardoublequote}% |
59 \begin{isamarkuptext}% |
57 \begin{isamarkuptext}% |
60 The definition \isa{prod{\isacharunderscore}bool{\isacharunderscore}def} becomes syntactically |
58 The definition \isa{prod{\isacharunderscore}bool{\isacharunderscore}def} becomes syntactically |
61 well-formed only after the arity \isa{bool\ {\isasymColon}\ product} is made |
59 well-formed only after the arity \isa{bool\ {\isasymColon}\ product} is made |