equal
deleted
inserted
replaced
15 |
15 |
16 The $product$ class below provides a less degenerate example of |
16 The $product$ class below provides a less degenerate example of |
17 syntactic type classes.% |
17 syntactic type classes.% |
18 \end{isamarkuptext}% |
18 \end{isamarkuptext}% |
19 \isacommand{axclass}\isanewline |
19 \isacommand{axclass}\isanewline |
20 \ \ product\ <\ {"}term{"}\isanewline |
20 \ \ product\ {\isacharless}\ {\isachardoublequote}term{\isachardoublequote}\isanewline |
21 \isacommand{consts}\isanewline |
21 \isacommand{consts}\isanewline |
22 \ \ product\ ::\ {"}'a::product\ {\isasymRightarrow}\ 'a\ {\isasymRightarrow}\ 'a{"}\ \ \ \ (\isakeyword{infixl}\ {"}{\isasymOtimes}{"}\ 70)% |
22 \ \ product\ ::\ {\isachardoublequote}{\isacharprime}a::product\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymOtimes}{\isachardoublequote}\ 70{\isacharparenright}% |
23 \begin{isamarkuptext}% |
23 \begin{isamarkuptext}% |
24 Here class $product$ is defined as subclass of $term$ without any |
24 Here class $product$ is defined as subclass of $term$ without any |
25 additional axioms. This effects in logical equivalence of $product$ |
25 additional axioms. This effects in logical equivalence of $product$ |
26 and $term$, as is reflected by the trivial introduction rule |
26 and $term$, as is reflected by the trivial introduction rule |
27 generated for this definition. |
27 generated for this definition. |
47 certain type $\tau$ do we instantiate $\tau :: c$. |
47 certain type $\tau$ do we instantiate $\tau :: c$. |
48 |
48 |
49 This is done for class $product$ and type $bool$ as follows.% |
49 This is done for class $product$ and type $bool$ as follows.% |
50 \end{isamarkuptext}% |
50 \end{isamarkuptext}% |
51 \isacommand{instance}\ bool\ ::\ product\isanewline |
51 \isacommand{instance}\ bool\ ::\ product\isanewline |
52 \ \ \isacommand{by}\ intro\_classes\isanewline |
52 \ \ \isacommand{by}\ intro{\isacharunderscore}classes\isanewline |
53 \isacommand{defs}\ (\isakeyword{overloaded})\isanewline |
53 \isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline |
54 \ \ product\_bool\_def:\ {"}x\ {\isasymOtimes}\ y\ {\isasymequiv}\ x\ {\isasymand}\ y{"}% |
54 \ \ product{\isacharunderscore}bool{\isacharunderscore}def:\ {\isachardoublequote}x\ {\isasymOtimes}\ y\ {\isasymequiv}\ x\ {\isasymand}\ y{\isachardoublequote}% |
55 \begin{isamarkuptext}% |
55 \begin{isamarkuptext}% |
56 The definition $prod_bool_def$ becomes syntactically well-formed only |
56 The definition $prod_bool_def$ becomes syntactically well-formed only |
57 after the arity $bool :: product$ is made known to the type checker. |
57 after the arity $bool :: product$ is made known to the type checker. |
58 |
58 |
59 \medskip It is very important to see that above $\DEFS$ are not |
59 \medskip It is very important to see that above $\DEFS$ are not |