15 |
15 |
16 We illustrate these basic concepts by the following formulation of |
16 We illustrate these basic concepts by the following formulation of |
17 semigroups.% |
17 semigroups.% |
18 \end{isamarkuptext}% |
18 \end{isamarkuptext}% |
19 \isacommand{consts}\isanewline |
19 \isacommand{consts}\isanewline |
20 \ \ 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 |
20 \ \ 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 |
21 \isacommand{axclass}\ semigroup\ {\isacharless}\ {\isachardoublequote}term{\isachardoublequote}\isanewline |
21 \isacommand{axclass}\ semigroup\ {\isacharless}\ {\isachardoublequote}term{\isachardoublequote}\isanewline |
22 \ \ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymodot}\ y{\isacharparenright}\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequote}% |
22 \ \ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymodot}\ y{\isacharparenright}\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequote}% |
23 \begin{isamarkuptext}% |
23 \begin{isamarkuptext}% |
24 \noindent Above we have first declared a polymorphic constant \isa{{\isasymodot}\ {\isasymColon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} and then defined the class \isa{semigroup} of |
24 \noindent Above we have first declared a polymorphic constant \isa{{\isasymodot}\ {\isasymColon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} and then defined the class \isa{semigroup} of |
25 all types \isa{{\isasymtau}} such that \isa{{\isasymodot}\ {\isasymColon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}} is indeed an |
25 all types \isa{{\isasymtau}} such that \isa{{\isasymodot}\ {\isasymColon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}} is indeed an |
34 Below, class \isa{plus{\isacharunderscore}semigroup} represents semigroups of the form |
34 Below, class \isa{plus{\isacharunderscore}semigroup} represents semigroups of the form |
35 \isa{{\isacharparenleft}{\isasymtau}{\isacharcomma}\ {\isasymoplus}{\isacharparenright}}, while the original \isa{semigroup} would |
35 \isa{{\isacharparenleft}{\isasymtau}{\isacharcomma}\ {\isasymoplus}{\isacharparenright}}, while the original \isa{semigroup} would |
36 correspond to semigroups \isa{{\isacharparenleft}{\isasymtau}{\isacharcomma}\ {\isasymodot}{\isacharparenright}}.% |
36 correspond to semigroups \isa{{\isacharparenleft}{\isasymtau}{\isacharcomma}\ {\isasymodot}{\isacharparenright}}.% |
37 \end{isamarkuptext}% |
37 \end{isamarkuptext}% |
38 \isacommand{consts}\isanewline |
38 \isacommand{consts}\isanewline |
39 \ \ plus\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymoplus}{\isachardoublequote}\ \isadigit{7}\isadigit{0}{\isacharparenright}\isanewline |
39 \ \ plus\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymoplus}{\isachardoublequote}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline |
40 \isacommand{axclass}\ plus{\isacharunderscore}semigroup\ {\isacharless}\ {\isachardoublequote}term{\isachardoublequote}\isanewline |
40 \isacommand{axclass}\ plus{\isacharunderscore}semigroup\ {\isacharless}\ {\isachardoublequote}term{\isachardoublequote}\isanewline |
41 \ \ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymoplus}\ y{\isacharparenright}\ {\isasymoplus}\ z\ {\isacharequal}\ x\ {\isasymoplus}\ {\isacharparenleft}y\ {\isasymoplus}\ z{\isacharparenright}{\isachardoublequote}% |
41 \ \ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymoplus}\ y{\isacharparenright}\ {\isasymoplus}\ z\ {\isacharequal}\ x\ {\isasymoplus}\ {\isacharparenleft}y\ {\isasymoplus}\ z{\isacharparenright}{\isachardoublequote}% |
42 \begin{isamarkuptext}% |
42 \begin{isamarkuptext}% |
43 \noindent Even if classes \isa{plus{\isacharunderscore}semigroup} and \isa{semigroup} both represent semigroups in a sense, they are certainly |
43 \noindent Even if classes \isa{plus{\isacharunderscore}semigroup} and \isa{semigroup} both represent semigroups in a sense, they are certainly |
44 not quite the same.% |
44 not quite the same.% |