19 \begin{isamarkuptext}% |
19 \begin{isamarkuptext}% |
20 First we declare some polymorphic constants required later for the |
20 First we declare some polymorphic constants required later for the |
21 signature parts of our structures.% |
21 signature parts of our structures.% |
22 \end{isamarkuptext}% |
22 \end{isamarkuptext}% |
23 \isacommand{consts}\isanewline |
23 \isacommand{consts}\isanewline |
24 \ \ times\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymodot}{\isachardoublequote}\ \isadigit{7}\isadigit{0}{\isacharparenright}\isanewline |
24 \ \ times\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymodot}{\isachardoublequote}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline |
25 \ \ inverse\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isacharparenleft}{\isacharunderscore}{\isasyminv}{\isacharparenright}{\isachardoublequote}\ {\isacharbrackleft}\isadigit{1}\isadigit{0}\isadigit{0}\isadigit{0}{\isacharbrackright}\ \isadigit{9}\isadigit{9}\isadigit{9}{\isacharparenright}\isanewline |
25 \ \ inverse\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isacharparenleft}{\isacharunderscore}{\isasyminv}{\isacharparenright}{\isachardoublequote}\ {\isacharbrackleft}{\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isacharbrackright}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharparenright}\isanewline |
26 \ \ one\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymunit}{\isachardoublequote}{\isacharparenright}% |
26 \ \ one\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymunit}{\isachardoublequote}{\isacharparenright}% |
27 \begin{isamarkuptext}% |
27 \begin{isamarkuptext}% |
28 \noindent Next we define class \isa{monoid} of monoids with |
28 \noindent Next we define class \isa{monoid} of monoids with |
29 operations \isa{{\isasymodot}} and \isa{{\isasymunit}}. Note that multiple class |
29 operations \isa{{\isasymodot}} and \isa{{\isasymunit}}. Note that multiple class |
30 axioms are allowed for user convenience --- they simply represent the |
30 axioms are allowed for user convenience --- they simply represent the |