equal
deleted
inserted
replaced
16 |
16 |
17 The \isa{product} class below provides a less degenerate example of |
17 The \isa{product} class below provides a less degenerate example of |
18 syntactic type classes.% |
18 syntactic type classes.% |
19 \end{isamarkuptext}% |
19 \end{isamarkuptext}% |
20 \isacommand{axclass}\isanewline |
20 \isacommand{axclass}\isanewline |
21 \ \ product\ {\isacharless}\ {\isachardoublequote}term{\isachardoublequote}\isanewline |
21 \ \ product\ {\isasymsubseteq}\ {\isachardoublequote}term{\isachardoublequote}\isanewline |
22 \isacommand{consts}\isanewline |
22 \isacommand{consts}\isanewline |
23 \ \ product\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a{\isasymColon}product\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymodot}{\isachardoublequote}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}% |
23 \ \ product\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a{\isasymColon}product\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymodot}{\isachardoublequote}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}% |
24 \begin{isamarkuptext}% |
24 \begin{isamarkuptext}% |
25 Here class \isa{product} is defined as subclass of \isa{term} |
25 Here class \isa{product} is defined as subclass of \isa{term} |
26 without any additional axioms. This effects in logical equivalence |
26 without any additional axioms. This effects in logical equivalence |