--- a/doc-src/Classes/Thy/document/Classes.tex Sun Nov 07 23:32:26 2010 +0100
+++ b/doc-src/Classes/Thy/document/Classes.tex Mon Nov 08 00:00:47 2010 +0100
@@ -28,8 +28,8 @@
of overloading\footnote{throughout this tutorial, we are referring
to classical Haskell 1.0 type classes, not considering later
additions in expressiveness}. As a canonical example, a polymorphic
- equality function \isa{eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} which is overloaded on
- different types for \isa{{\isasymalpha}}, which is achieved by splitting
+ equality function \isa{eq\ {\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool} which is overloaded on
+ different types for \isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}}, which is achieved by splitting
introduction of the \isa{eq} function from its overloaded
definitions by means of \isa{class} and \isa{instance}
declarations: \footnote{syntax here is a kind of isabellized
@@ -38,20 +38,20 @@
\begin{quote}
\noindent\isa{class\ eq\ where} \\
- \hspace*{2ex}\isa{eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool}
+ \hspace*{2ex}\isa{eq\ {\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}
- \medskip\noindent\isa{instance\ nat\ {\isasymColon}\ eq\ where} \\
- \hspace*{2ex}\isa{eq\ {\isadigit{0}}\ {\isadigit{0}}\ {\isacharequal}\ True} \\
- \hspace*{2ex}\isa{eq\ {\isadigit{0}}\ {\isacharunderscore}\ {\isacharequal}\ False} \\
- \hspace*{2ex}\isa{eq\ {\isacharunderscore}\ {\isadigit{0}}\ {\isacharequal}\ False} \\
- \hspace*{2ex}\isa{eq\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharparenleft}Suc\ m{\isacharparenright}\ {\isacharequal}\ eq\ n\ m}
+ \medskip\noindent\isa{instance\ nat\ {\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}\ eq\ where} \\
+ \hspace*{2ex}\isa{eq\ {\isadigit{0}}\ {\isadigit{0}}\ {\isaliteral{3D}{\isacharequal}}\ True} \\
+ \hspace*{2ex}\isa{eq\ {\isadigit{0}}\ {\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{3D}{\isacharequal}}\ False} \\
+ \hspace*{2ex}\isa{eq\ {\isaliteral{5F}{\isacharunderscore}}\ {\isadigit{0}}\ {\isaliteral{3D}{\isacharequal}}\ False} \\
+ \hspace*{2ex}\isa{eq\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}Suc\ m{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ eq\ n\ m}
- \medskip\noindent\isa{instance\ {\isacharparenleft}{\isasymalpha}{\isasymColon}eq{\isacharcomma}\ {\isasymbeta}{\isasymColon}eq{\isacharparenright}\ pair\ {\isasymColon}\ eq\ where} \\
- \hspace*{2ex}\isa{eq\ {\isacharparenleft}x{\isadigit{1}}{\isacharcomma}\ y{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ eq\ x{\isadigit{1}}\ x{\isadigit{2}}\ {\isasymand}\ eq\ y{\isadigit{1}}\ y{\isadigit{2}}}
+ \medskip\noindent\isa{instance\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}eq{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C626574613E}{\isasymbeta}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}eq{\isaliteral{29}{\isacharparenright}}\ pair\ {\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}\ eq\ where} \\
+ \hspace*{2ex}\isa{eq\ {\isaliteral{28}{\isacharparenleft}}x{\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ y{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}x{\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}\ y{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ eq\ x{\isadigit{1}}\ x{\isadigit{2}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ eq\ y{\isadigit{1}}\ y{\isadigit{2}}}
\medskip\noindent\isa{class\ ord\ extends\ eq\ where} \\
- \hspace*{2ex}\isa{less{\isacharunderscore}eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} \\
- \hspace*{2ex}\isa{less\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool}
+ \hspace*{2ex}\isa{less{\isaliteral{5F}{\isacharunderscore}}eq\ {\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool} \\
+ \hspace*{2ex}\isa{less\ {\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}
\end{quote}
@@ -75,11 +75,11 @@
\begin{quote}
\noindent\isa{class\ eq\ where} \\
- \hspace*{2ex}\isa{eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} \\
+ \hspace*{2ex}\isa{eq\ {\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool} \\
\isa{satisfying} \\
- \hspace*{2ex}\isa{refl{\isacharcolon}\ eq\ x\ x} \\
- \hspace*{2ex}\isa{sym{\isacharcolon}\ eq\ x\ y\ {\isasymlongleftrightarrow}\ eq\ x\ y} \\
- \hspace*{2ex}\isa{trans{\isacharcolon}\ eq\ x\ y\ {\isasymand}\ eq\ y\ z\ {\isasymlongrightarrow}\ eq\ x\ z}
+ \hspace*{2ex}\isa{refl{\isaliteral{3A}{\isacharcolon}}\ eq\ x\ x} \\
+ \hspace*{2ex}\isa{sym{\isaliteral{3A}{\isacharcolon}}\ eq\ x\ y\ {\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}\ eq\ x\ y} \\
+ \hspace*{2ex}\isa{trans{\isaliteral{3A}{\isacharcolon}}\ eq\ x\ y\ {\isaliteral{5C3C616E643E}{\isasymand}}\ eq\ y\ z\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ eq\ x\ z}
\end{quote}
@@ -119,7 +119,7 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Depending on an arbitrary type \isa{{\isasymalpha}}, class \isa{semigroup} introduces a binary operator \isa{{\isacharparenleft}{\isasymotimes}{\isacharparenright}} that is
+Depending on an arbitrary type \isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}}, class \isa{semigroup} introduces a binary operator \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}{\isaliteral{29}{\isacharparenright}}} that is
assumed to be associative:%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -130,9 +130,9 @@
%
\isatagquote
\isacommand{class}\isamarkupfalse%
-\ semigroup\ {\isacharequal}\isanewline
-\ \ \isakeyword{fixes}\ mult\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymotimes}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline
-\ \ \isakeyword{assumes}\ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isasymotimes}\ z\ {\isacharequal}\ x\ {\isasymotimes}\ {\isacharparenleft}y\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}%
+\ semigroup\ {\isaliteral{3D}{\isacharequal}}\isanewline
+\ \ \isakeyword{fixes}\ mult\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{22}{\isachardoublequoteclose}}\ \ \ \ {\isaliteral{28}{\isacharparenleft}}\isakeyword{infixl}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isadigit{7}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline
+\ \ \isakeyword{assumes}\ assoc{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ z\ {\isaliteral{3D}{\isacharequal}}\ x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ {\isaliteral{28}{\isacharparenleft}}y\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ z{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
\endisatagquote
{\isafoldquote}%
%
@@ -144,8 +144,8 @@
\noindent This \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}} specification consists of two parts:
the \qn{operational} part names the class parameter (\hyperlink{element.fixes}{\mbox{\isa{\isakeyword{fixes}}}}), the \qn{logical} part specifies properties on them
(\hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}}). The local \hyperlink{element.fixes}{\mbox{\isa{\isakeyword{fixes}}}} and \hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}} are lifted to the theory toplevel, yielding the global
- parameter \isa{{\isachardoublequote}mult\ {\isasymColon}\ {\isasymalpha}{\isasymColon}semigroup\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequote}} and the
- global theorem \hyperlink{fact.semigroup.assoc:}{\mbox{\isa{semigroup{\isachardot}assoc{\isacharcolon}}}}~\isa{{\isachardoublequote}{\isasymAnd}x\ y\ z\ {\isasymColon}\ {\isasymalpha}{\isasymColon}semigroup{\isachardot}\ {\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isasymotimes}\ z\ {\isacharequal}\ x\ {\isasymotimes}\ {\isacharparenleft}y\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequote}}.%
+ parameter \isa{{\isaliteral{22}{\isachardoublequote}}mult\ {\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}semigroup\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{22}{\isachardoublequote}}} and the
+ global theorem \hyperlink{fact.semigroup.assoc:}{\mbox{\isa{semigroup{\isaliteral{2E}{\isachardot}}assoc{\isaliteral{3A}{\isacharcolon}}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x\ y\ z\ {\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}semigroup{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ z\ {\isaliteral{3D}{\isacharequal}}\ x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ {\isaliteral{28}{\isacharparenleft}}y\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ z{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -155,7 +155,7 @@
%
\begin{isamarkuptext}%
The concrete type \isa{int} is made a \isa{semigroup} instance
- by providing a suitable definition for the class parameter \isa{{\isacharparenleft}{\isasymotimes}{\isacharparenright}} and a proof for the specification of \hyperlink{fact.assoc}{\mbox{\isa{assoc}}}. This is
+ by providing a suitable definition for the class parameter \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}{\isaliteral{29}{\isacharparenright}}} and a proof for the specification of \hyperlink{fact.assoc}{\mbox{\isa{assoc}}}. This is
accomplished by the \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}} target:%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -166,25 +166,25 @@
%
\isatagquote
\isacommand{instantiation}\isamarkupfalse%
-\ int\ {\isacharcolon}{\isacharcolon}\ semigroup\isanewline
+\ int\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ semigroup\isanewline
\isakeyword{begin}\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
\isanewline
-\ \ mult{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}i\ {\isasymotimes}\ j\ {\isacharequal}\ i\ {\isacharplus}\ {\isacharparenleft}j{\isasymColon}int{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ mult{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}i\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ j\ {\isaliteral{3D}{\isacharequal}}\ i\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{28}{\isacharparenleft}}j{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}int{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\isanewline
\isacommand{instance}\isamarkupfalse%
\ \isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
-\ i\ j\ k\ {\isacharcolon}{\isacharcolon}\ int\ \isacommand{have}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isacharparenleft}i\ {\isacharplus}\ j{\isacharparenright}\ {\isacharplus}\ k\ {\isacharequal}\ i\ {\isacharplus}\ {\isacharparenleft}j\ {\isacharplus}\ k{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
+\ i\ j\ k\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ int\ \isacommand{have}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}i\ {\isaliteral{2B}{\isacharplus}}\ j{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\ k\ {\isaliteral{3D}{\isacharequal}}\ i\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{28}{\isacharparenleft}}j\ {\isaliteral{2B}{\isacharplus}}\ k{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isacharparenleft}i\ {\isasymotimes}\ j{\isacharparenright}\ {\isasymotimes}\ k\ {\isacharequal}\ i\ {\isasymotimes}\ {\isacharparenleft}j\ {\isasymotimes}\ k{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}i\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ j{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ k\ {\isaliteral{3D}{\isacharequal}}\ i\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ {\isaliteral{28}{\isacharparenleft}}j\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ k{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
-\ mult{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{{\isachardot}}\isamarkupfalse%
+\ mult{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{5F}{\isacharunderscore}}def\ \isacommand{{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
\isanewline
@@ -203,7 +203,7 @@
particular instance using common specification tools (here,
\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}). The concluding \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} opens a
proof that the given parameters actually conform to the class
- specification. Note that the first proof step is the \hyperlink{method.default}{\mbox{\isa{default}}} method, which for such instance proofs maps to the \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}} method. This reduces an instance judgement to the
+ specification. Note that the first proof step is the \hyperlink{method.default}{\mbox{\isa{default}}} method, which for such instance proofs maps to the \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isaliteral{5F}{\isacharunderscore}}classes}}} method. This reduces an instance judgement to the
relevant primitive proof goals; typically it is the first method
applied in an instantiation proof.
@@ -221,23 +221,23 @@
%
\isatagquote
\isacommand{instantiation}\isamarkupfalse%
-\ nat\ {\isacharcolon}{\isacharcolon}\ semigroup\isanewline
+\ nat\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ semigroup\isanewline
\isakeyword{begin}\isanewline
\isanewline
\isacommand{primrec}\isamarkupfalse%
-\ mult{\isacharunderscore}nat\ \isakeyword{where}\isanewline
-\ \ {\isachardoublequoteopen}{\isacharparenleft}{\isadigit{0}}{\isasymColon}nat{\isacharparenright}\ {\isasymotimes}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
-\ \ {\isacharbar}\ {\isachardoublequoteopen}Suc\ m\ {\isasymotimes}\ n\ {\isacharequal}\ Suc\ {\isacharparenleft}m\ {\isasymotimes}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ mult{\isaliteral{5F}{\isacharunderscore}}nat\ \isakeyword{where}\isanewline
+\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}nat{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ n\ {\isaliteral{3D}{\isacharequal}}\ n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ \ {\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}Suc\ m\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ n\ {\isaliteral{3D}{\isacharequal}}\ Suc\ {\isaliteral{28}{\isacharparenleft}}m\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\isanewline
\isacommand{instance}\isamarkupfalse%
\ \isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
-\ m\ n\ q\ {\isacharcolon}{\isacharcolon}\ nat\ \isanewline
+\ m\ n\ q\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ nat\ \isanewline
\ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}m\ {\isasymotimes}\ n\ {\isasymotimes}\ q\ {\isacharequal}\ m\ {\isasymotimes}\ {\isacharparenleft}n\ {\isasymotimes}\ q{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}m\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ n\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ q\ {\isaliteral{3D}{\isacharequal}}\ m\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ q{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}induct\ m{\isacharparenright}\ auto\isanewline
+\ {\isaliteral{28}{\isacharparenleft}}induct\ m{\isaliteral{29}{\isacharparenright}}\ auto\isanewline
\isacommand{qed}\isamarkupfalse%
\isanewline
\isanewline
@@ -251,11 +251,11 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\noindent Note the occurence of the name \isa{mult{\isacharunderscore}nat} in the
+\noindent Note the occurence of the name \isa{mult{\isaliteral{5F}{\isacharunderscore}}nat} in the
primrec declaration; by default, the local name of a class operation
- \isa{f} to be instantiated on type constructor \isa{{\isasymkappa}} is
- mangled as \isa{f{\isacharunderscore}{\isasymkappa}}. In case of uncertainty, these names may be
- inspected using the \hyperlink{command.print-context}{\mbox{\isa{\isacommand{print{\isacharunderscore}context}}}} command or the
+ \isa{f} to be instantiated on type constructor \isa{{\isaliteral{5C3C6B617070613E}{\isasymkappa}}} is
+ mangled as \isa{f{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{5C3C6B617070613E}{\isasymkappa}}}. In case of uncertainty, these names may be
+ inspected using the \hyperlink{command.print-context}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}context}}}} command or the
corresponding ProofGeneral button.%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -277,23 +277,23 @@
%
\isatagquote
\isacommand{instantiation}\isamarkupfalse%
-\ prod\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}semigroup{\isacharcomma}\ semigroup{\isacharparenright}\ semigroup\isanewline
+\ prod\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}semigroup{\isaliteral{2C}{\isacharcomma}}\ semigroup{\isaliteral{29}{\isacharparenright}}\ semigroup\isanewline
\isakeyword{begin}\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
\isanewline
-\ \ mult{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{2}}\ {\isacharequal}\ {\isacharparenleft}fst\ p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ fst\ p\isactrlisub {\isadigit{2}}{\isacharcomma}\ snd\ p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ snd\ p\isactrlisub {\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ mult{\isaliteral{5F}{\isacharunderscore}}prod{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}p\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ p\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}fst\ p\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ fst\ p\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}\ snd\ p\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ snd\ p\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\isanewline
\isacommand{instance}\isamarkupfalse%
\ \isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
-\ p\isactrlisub {\isadigit{1}}\ p\isactrlisub {\isadigit{2}}\ p\isactrlisub {\isadigit{3}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isasymColon}semigroup\ {\isasymtimes}\ {\isasymbeta}{\isasymColon}semigroup{\isachardoublequoteclose}\isanewline
+\ p\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ p\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}\ p\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{3}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}semigroup\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{5C3C626574613E}{\isasymbeta}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}semigroup{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{2}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{3}}\ {\isacharequal}\ p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ {\isacharparenleft}p\isactrlisub {\isadigit{2}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{3}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}p\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ p\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ p\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{3}}\ {\isaliteral{3D}{\isacharequal}}\ p\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ {\isaliteral{28}{\isacharparenleft}}p\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ p\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{3}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
-\ mult{\isacharunderscore}prod{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}simp\ add{\isacharcolon}\ assoc{\isacharparenright}\isanewline
+\ mult{\isaliteral{5F}{\isacharunderscore}}prod{\isaliteral{5F}{\isacharunderscore}}def\ \isacommand{by}\isamarkupfalse%
+\ {\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ assoc{\isaliteral{29}{\isacharparenright}}\isanewline
\isacommand{qed}\isamarkupfalse%
\ \ \ \ \ \ \isanewline
\isanewline
@@ -308,7 +308,7 @@
%
\begin{isamarkuptext}%
\noindent Associativity of product semigroups is established using
- the definition of \isa{{\isacharparenleft}{\isasymotimes}{\isacharparenright}} on products and the hypothetical
+ the definition of \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}{\isaliteral{29}{\isacharparenright}}} on products and the hypothetical
associativity of the type components; these hypotheses are
legitimate due to the \isa{semigroup} constraints imposed on the
type components by the \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} proposition. Indeed,
@@ -333,9 +333,9 @@
%
\isatagquote
\isacommand{class}\isamarkupfalse%
-\ monoidl\ {\isacharequal}\ semigroup\ {\isacharplus}\isanewline
-\ \ \isakeyword{fixes}\ neutral\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isachardoublequoteclose}\ {\isacharparenleft}{\isachardoublequoteopen}{\isasymone}{\isachardoublequoteclose}{\isacharparenright}\isanewline
-\ \ \isakeyword{assumes}\ neutl{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}%
+\ monoidl\ {\isaliteral{3D}{\isacharequal}}\ semigroup\ {\isaliteral{2B}{\isacharplus}}\isanewline
+\ \ \isakeyword{fixes}\ neutral\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6F6E653E}{\isasymone}}{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}\isanewline
+\ \ \isakeyword{assumes}\ neutl{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6F6E653E}{\isasymone}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ x\ {\isaliteral{3D}{\isacharequal}}\ x{\isaliteral{22}{\isachardoublequoteclose}}%
\endisatagquote
{\isafoldquote}%
%
@@ -357,35 +357,35 @@
%
\isatagquote
\isacommand{instantiation}\isamarkupfalse%
-\ nat\ \isakeyword{and}\ int\ {\isacharcolon}{\isacharcolon}\ monoidl\isanewline
+\ nat\ \isakeyword{and}\ int\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ monoidl\isanewline
\isakeyword{begin}\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
\isanewline
-\ \ neutral{\isacharunderscore}nat{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}nat{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ neutral{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6F6E653E}{\isasymone}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}nat{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
\isanewline
-\ \ neutral{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}int{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ neutral{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6F6E653E}{\isasymone}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}int{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\isanewline
\isacommand{instance}\isamarkupfalse%
\ \isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
-\ n\ {\isacharcolon}{\isacharcolon}\ nat\isanewline
+\ n\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ nat\isanewline
\ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6F6E653E}{\isasymone}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ n\ {\isaliteral{3D}{\isacharequal}}\ n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
-\ neutral{\isacharunderscore}nat{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
+\ neutral{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{5F}{\isacharunderscore}}def\ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
-\ k\ {\isacharcolon}{\isacharcolon}\ int\isanewline
+\ k\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ int\isanewline
\ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ k\ {\isacharequal}\ k{\isachardoublequoteclose}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6F6E653E}{\isasymone}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ k\ {\isaliteral{3D}{\isacharequal}}\ k{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
-\ neutral{\isacharunderscore}int{\isacharunderscore}def\ mult{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
+\ neutral{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{5F}{\isacharunderscore}}def\ mult{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{5F}{\isacharunderscore}}def\ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\isacommand{qed}\isamarkupfalse%
\isanewline
@@ -394,23 +394,23 @@
\isanewline
\isanewline
\isacommand{instantiation}\isamarkupfalse%
-\ prod\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}monoidl{\isacharcomma}\ monoidl{\isacharparenright}\ monoidl\isanewline
+\ prod\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}monoidl{\isaliteral{2C}{\isacharcomma}}\ monoidl{\isaliteral{29}{\isacharparenright}}\ monoidl\isanewline
\isakeyword{begin}\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
\isanewline
-\ \ neutral{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isacharequal}\ {\isacharparenleft}{\isasymone}{\isacharcomma}\ {\isasymone}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ neutral{\isaliteral{5F}{\isacharunderscore}}prod{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6F6E653E}{\isasymone}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6F6E653E}{\isasymone}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C6F6E653E}{\isasymone}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\isanewline
\isacommand{instance}\isamarkupfalse%
\ \isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
-\ p\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isasymColon}monoidl\ {\isasymtimes}\ {\isasymbeta}{\isasymColon}monoidl{\isachardoublequoteclose}\isanewline
+\ p\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}monoidl\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{5C3C626574613E}{\isasymbeta}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}monoidl{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ p\ {\isacharequal}\ p{\isachardoublequoteclose}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6F6E653E}{\isasymone}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ p\ {\isaliteral{3D}{\isacharequal}}\ p{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
-\ neutral{\isacharunderscore}prod{\isacharunderscore}def\ mult{\isacharunderscore}prod{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}simp\ add{\isacharcolon}\ neutl{\isacharparenright}\isanewline
+\ neutral{\isaliteral{5F}{\isacharunderscore}}prod{\isaliteral{5F}{\isacharunderscore}}def\ mult{\isaliteral{5F}{\isacharunderscore}}prod{\isaliteral{5F}{\isacharunderscore}}def\ \isacommand{by}\isamarkupfalse%
+\ {\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ neutl{\isaliteral{29}{\isacharparenright}}\isanewline
\isacommand{qed}\isamarkupfalse%
\isanewline
\isanewline
@@ -435,31 +435,31 @@
%
\isatagquote
\isacommand{class}\isamarkupfalse%
-\ monoid\ {\isacharequal}\ monoidl\ {\isacharplus}\isanewline
-\ \ \isakeyword{assumes}\ neutr{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline
+\ monoid\ {\isaliteral{3D}{\isacharequal}}\ monoidl\ {\isaliteral{2B}{\isacharplus}}\isanewline
+\ \ \isakeyword{assumes}\ neutr{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ {\isaliteral{5C3C6F6E653E}{\isasymone}}\ {\isaliteral{3D}{\isacharequal}}\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\isanewline
\isacommand{instantiation}\isamarkupfalse%
-\ nat\ \isakeyword{and}\ int\ {\isacharcolon}{\isacharcolon}\ monoid\ \isanewline
+\ nat\ \isakeyword{and}\ int\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ monoid\ \isanewline
\isakeyword{begin}\isanewline
\isanewline
\isacommand{instance}\isamarkupfalse%
\ \isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
-\ n\ {\isacharcolon}{\isacharcolon}\ nat\isanewline
+\ n\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ nat\isanewline
\ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}n\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}n\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ {\isaliteral{5C3C6F6E653E}{\isasymone}}\ {\isaliteral{3D}{\isacharequal}}\ n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
-\ neutral{\isacharunderscore}nat{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}induct\ n{\isacharparenright}\ simp{\isacharunderscore}all\isanewline
+\ neutral{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{5F}{\isacharunderscore}}def\ \isacommand{by}\isamarkupfalse%
+\ {\isaliteral{28}{\isacharparenleft}}induct\ n{\isaliteral{29}{\isacharparenright}}\ simp{\isaliteral{5F}{\isacharunderscore}}all\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
-\ k\ {\isacharcolon}{\isacharcolon}\ int\isanewline
+\ k\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ int\isanewline
\ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}k\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ k{\isachardoublequoteclose}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}k\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ {\isaliteral{5C3C6F6E653E}{\isasymone}}\ {\isaliteral{3D}{\isacharequal}}\ k{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
-\ neutral{\isacharunderscore}int{\isacharunderscore}def\ mult{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
+\ neutral{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{5F}{\isacharunderscore}}def\ mult{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{5F}{\isacharunderscore}}def\ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\isacommand{qed}\isamarkupfalse%
\isanewline
@@ -468,19 +468,19 @@
\isanewline
\isanewline
\isacommand{instantiation}\isamarkupfalse%
-\ prod\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}monoid{\isacharcomma}\ monoid{\isacharparenright}\ monoid\isanewline
+\ prod\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}monoid{\isaliteral{2C}{\isacharcomma}}\ monoid{\isaliteral{29}{\isacharparenright}}\ monoid\isanewline
\isakeyword{begin}\isanewline
\isanewline
\isacommand{instance}\isamarkupfalse%
\ \isacommand{proof}\isamarkupfalse%
\ \isanewline
\ \ \isacommand{fix}\isamarkupfalse%
-\ p\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isasymColon}monoid\ {\isasymtimes}\ {\isasymbeta}{\isasymColon}monoid{\isachardoublequoteclose}\isanewline
+\ p\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}monoid\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{5C3C626574613E}{\isasymbeta}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}monoid{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}p\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ p{\isachardoublequoteclose}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}p\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ {\isaliteral{5C3C6F6E653E}{\isasymone}}\ {\isaliteral{3D}{\isacharequal}}\ p{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
-\ neutral{\isacharunderscore}prod{\isacharunderscore}def\ mult{\isacharunderscore}prod{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}simp\ add{\isacharcolon}\ neutr{\isacharparenright}\isanewline
+\ neutral{\isaliteral{5F}{\isacharunderscore}}prod{\isaliteral{5F}{\isacharunderscore}}def\ mult{\isaliteral{5F}{\isacharunderscore}}prod{\isaliteral{5F}{\isacharunderscore}}def\ \isacommand{by}\isamarkupfalse%
+\ {\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ neutr{\isaliteral{29}{\isacharparenright}}\isanewline
\isacommand{qed}\isamarkupfalse%
\isanewline
\isanewline
@@ -504,31 +504,31 @@
%
\isatagquote
\isacommand{class}\isamarkupfalse%
-\ group\ {\isacharequal}\ monoidl\ {\isacharplus}\isanewline
-\ \ \isakeyword{fixes}\ inverse\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}{\isachardoublequoteopen}{\isacharparenleft}{\isacharunderscore}{\isasymdiv}{\isacharparenright}{\isachardoublequoteclose}\ {\isacharbrackleft}{\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isacharbrackright}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharparenright}\isanewline
-\ \ \isakeyword{assumes}\ invl{\isacharcolon}\ {\isachardoublequoteopen}x{\isasymdiv}\ {\isasymotimes}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline
+\ group\ {\isaliteral{3D}{\isacharequal}}\ monoidl\ {\isaliteral{2B}{\isacharplus}}\isanewline
+\ \ \isakeyword{fixes}\ inverse\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{22}{\isachardoublequoteclose}}\ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{5C3C6469763E}{\isasymdiv}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isaliteral{5D}{\isacharbrackright}}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isaliteral{29}{\isacharparenright}}\isanewline
+\ \ \isakeyword{assumes}\ invl{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}x{\isaliteral{5C3C6469763E}{\isasymdiv}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ x\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C6F6E653E}{\isasymone}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\isanewline
\isacommand{instantiation}\isamarkupfalse%
-\ int\ {\isacharcolon}{\isacharcolon}\ group\isanewline
+\ int\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ group\isanewline
\isakeyword{begin}\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
\isanewline
-\ \ inverse{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}i{\isasymdiv}\ {\isacharequal}\ {\isacharminus}\ {\isacharparenleft}i{\isasymColon}int{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ inverse{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}i{\isaliteral{5C3C6469763E}{\isasymdiv}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{28}{\isacharparenleft}}i{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}int{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\isanewline
\isacommand{instance}\isamarkupfalse%
\ \isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
-\ i\ {\isacharcolon}{\isacharcolon}\ int\isanewline
+\ i\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ int\isanewline
\ \ \isacommand{have}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isacharminus}i\ {\isacharplus}\ i\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{2D}{\isacharminus}}i\ {\isaliteral{2B}{\isacharplus}}\ i\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}i{\isasymdiv}\ {\isasymotimes}\ i\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}i{\isaliteral{5C3C6469763E}{\isasymdiv}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ i\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C6F6E653E}{\isasymone}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
-\ mult{\isacharunderscore}int{\isacharunderscore}def\ neutral{\isacharunderscore}int{\isacharunderscore}def\ inverse{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{{\isachardot}}\isamarkupfalse%
+\ mult{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{5F}{\isacharunderscore}}def\ neutral{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{5F}{\isacharunderscore}}def\ inverse{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{5F}{\isacharunderscore}}def\ \isacommand{{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
\isanewline
@@ -564,9 +564,9 @@
%
\isatagquote
\isacommand{class}\isamarkupfalse%
-\ idem\ {\isacharequal}\isanewline
-\ \ \isakeyword{fixes}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\isanewline
-\ \ \isakeyword{assumes}\ idem{\isacharcolon}\ {\isachardoublequoteopen}f\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharequal}\ f\ x{\isachardoublequoteclose}%
+\ idem\ {\isaliteral{3D}{\isacharequal}}\isanewline
+\ \ \isakeyword{fixes}\ f\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ \ \isakeyword{assumes}\ idem{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}f\ {\isaliteral{28}{\isacharparenleft}}f\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ f\ x{\isaliteral{22}{\isachardoublequoteclose}}%
\endisatagquote
{\isafoldquote}%
%
@@ -598,9 +598,9 @@
%
\isatagquote
\isacommand{locale}\isamarkupfalse%
-\ idem\ {\isacharequal}\isanewline
-\ \ \isakeyword{fixes}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\isanewline
-\ \ \isakeyword{assumes}\ idem{\isacharcolon}\ {\isachardoublequoteopen}f\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharequal}\ f\ x{\isachardoublequoteclose}%
+\ idem\ {\isaliteral{3D}{\isacharequal}}\isanewline
+\ \ \isakeyword{fixes}\ f\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ \ \isakeyword{assumes}\ idem{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}f\ {\isaliteral{28}{\isacharparenleft}}f\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ f\ x{\isaliteral{22}{\isachardoublequoteclose}}%
\endisatagquote
{\isafoldquote}%
%
@@ -619,7 +619,7 @@
%
\isatagquote
\isacommand{consts}\isamarkupfalse%
-\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}%
+\ f\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{22}{\isachardoublequoteclose}}%
\endisatagquote
{\isafoldquote}%
%
@@ -652,7 +652,7 @@
%
\isatagquote
\isacommand{classes}\isamarkupfalse%
-\ idem\ {\isacharless}\ type%
+\ idem\ {\isaliteral{3C}{\isacharless}}\ type%
\endisatagquote
{\isafoldquote}%
%
@@ -684,8 +684,8 @@
%
\isatagquote
\isacommand{interpretation}\isamarkupfalse%
-\ idem{\isacharunderscore}class{\isacharcolon}\isanewline
-\ \ idem\ {\isachardoublequoteopen}f\ {\isasymColon}\ {\isacharparenleft}{\isasymalpha}{\isasymColon}idem{\isacharparenright}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}%
+\ idem{\isaliteral{5F}{\isacharunderscore}}class{\isaliteral{3A}{\isacharcolon}}\isanewline
+\ \ idem\ {\isaliteral{22}{\isachardoublequoteopen}}f\ {\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}idem{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{22}{\isachardoublequoteclose}}%
\endisatagquote
{\isafoldquote}%
%
@@ -720,8 +720,8 @@
\begin{isamarkuptext}%
Isabelle locales enable reasoning at a general level, while results
are implicitly transferred to all instances. For example, we can
- now establish the \isa{left{\isacharunderscore}cancel} lemma for groups, which
- states that the function \isa{{\isacharparenleft}x\ {\isasymotimes}{\isacharparenright}} is injective:%
+ now establish the \isa{left{\isaliteral{5F}{\isacharunderscore}}cancel} lemma for groups, which
+ states that the function \isa{{\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}{\isaliteral{29}{\isacharparenright}}} is injective:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -731,32 +731,32 @@
%
\isatagquote
\isacommand{lemma}\isamarkupfalse%
-\ {\isacharparenleft}\isakeyword{in}\ group{\isacharparenright}\ left{\isacharunderscore}cancel{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequoteclose}\isanewline
+\ {\isaliteral{28}{\isacharparenleft}}\isakeyword{in}\ group{\isaliteral{29}{\isacharparenright}}\ left{\isaliteral{5F}{\isacharunderscore}}cancel{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ y\ {\isaliteral{3D}{\isacharequal}}\ x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ z\ {\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}\ y\ {\isaliteral{3D}{\isacharequal}}\ z{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
-\ {\isachardoublequoteopen}x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z{\isachardoublequoteclose}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ y\ {\isaliteral{3D}{\isacharequal}}\ x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ z{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{have}\isamarkupfalse%
-\ {\isachardoublequoteopen}x{\isasymdiv}\ {\isasymotimes}\ {\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isacharequal}\ x{\isasymdiv}\ {\isasymotimes}\ {\isacharparenleft}x\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}x{\isaliteral{5C3C6469763E}{\isasymdiv}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ x{\isaliteral{5C3C6469763E}{\isasymdiv}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ z{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{have}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isacharparenleft}x{\isasymdiv}\ {\isasymotimes}\ x{\isacharparenright}\ {\isasymotimes}\ y\ {\isacharequal}\ {\isacharparenleft}x{\isasymdiv}\ {\isasymotimes}\ x{\isacharparenright}\ {\isasymotimes}\ z{\isachardoublequoteclose}\ \isacommand{using}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{5C3C6469763E}{\isasymdiv}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ y\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{5C3C6469763E}{\isasymdiv}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ z{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{using}\isamarkupfalse%
\ assoc\ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}y\ {\isacharequal}\ z{\isachardoublequoteclose}\ \isacommand{using}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}y\ {\isaliteral{3D}{\isacharequal}}\ z{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{using}\isamarkupfalse%
\ neutl\ \isakeyword{and}\ invl\ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
-\ {\isachardoublequoteopen}y\ {\isacharequal}\ z{\isachardoublequoteclose}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}y\ {\isaliteral{3D}{\isacharequal}}\ z{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ y\ {\isaliteral{3D}{\isacharequal}}\ x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ z{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\isacommand{qed}\isamarkupfalse%
%
@@ -771,9 +771,9 @@
\noindent Here the \qt{\hyperlink{keyword.in}{\mbox{\isa{\isakeyword{in}}}} \isa{group}} target
specification indicates that the result is recorded within that
context for later use. This local theorem is also lifted to the
- global one \hyperlink{fact.group.left-cancel:}{\mbox{\isa{group{\isachardot}left{\isacharunderscore}cancel{\isacharcolon}}}} \isa{{\isachardoublequote}{\isasymAnd}x\ y\ z\ {\isasymColon}\ {\isasymalpha}{\isasymColon}group{\isachardot}\ x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequote}}. Since type \isa{int} has been
+ global one \hyperlink{fact.group.left-cancel:}{\mbox{\isa{group{\isaliteral{2E}{\isachardot}}left{\isaliteral{5F}{\isacharunderscore}}cancel{\isaliteral{3A}{\isacharcolon}}}}} \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x\ y\ z\ {\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}group{\isaliteral{2E}{\isachardot}}\ x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ y\ {\isaliteral{3D}{\isacharequal}}\ x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ z\ {\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}\ y\ {\isaliteral{3D}{\isacharequal}}\ z{\isaliteral{22}{\isachardoublequote}}}. Since type \isa{int} has been
made an instance of \isa{group} before, we may refer to that
- fact as well: \isa{{\isachardoublequote}{\isasymAnd}x\ y\ z\ {\isasymColon}\ int{\isachardot}\ x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequote}}.%
+ fact as well: \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x\ y\ z\ {\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}\ int{\isaliteral{2E}{\isachardot}}\ x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ y\ {\isaliteral{3D}{\isacharequal}}\ x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ z\ {\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}\ y\ {\isaliteral{3D}{\isacharequal}}\ z{\isaliteral{22}{\isachardoublequote}}}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -792,9 +792,9 @@
%
\isatagquote
\isacommand{primrec}\isamarkupfalse%
-\ {\isacharparenleft}\isakeyword{in}\ monoid{\isacharparenright}\ pow{\isacharunderscore}nat\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-\ \ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isadigit{0}}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline
-\ \ {\isacharbar}\ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isacharparenleft}Suc\ n{\isacharparenright}\ x\ {\isacharequal}\ x\ {\isasymotimes}\ pow{\isacharunderscore}nat\ n\ x{\isachardoublequoteclose}%
+\ {\isaliteral{28}{\isacharparenleft}}\isakeyword{in}\ monoid{\isaliteral{29}{\isacharparenright}}\ pow{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
+\ \ {\isaliteral{22}{\isachardoublequoteopen}}pow{\isaliteral{5F}{\isacharunderscore}}nat\ {\isadigit{0}}\ x\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C6F6E653E}{\isasymone}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ \ {\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}pow{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\ x\ {\isaliteral{3D}{\isacharequal}}\ x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ pow{\isaliteral{5F}{\isacharunderscore}}nat\ n\ x{\isaliteral{22}{\isachardoublequoteclose}}%
\endisatagquote
{\isafoldquote}%
%
@@ -804,10 +804,10 @@
%
\begin{isamarkuptext}%
\noindent If the locale \isa{group} is also a class, this local
- definition is propagated onto a global definition of \isa{{\isachardoublequote}pow{\isacharunderscore}nat\ {\isasymColon}\ nat\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}monoid\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}monoid{\isachardoublequote}} with corresponding theorems
+ definition is propagated onto a global definition of \isa{{\isaliteral{22}{\isachardoublequote}}pow{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}\ nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}monoid\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}monoid{\isaliteral{22}{\isachardoublequote}}} with corresponding theorems
- \isa{pow{\isacharunderscore}nat\ {\isadigit{0}}\ x\ {\isacharequal}\ {\isasymone}\isasep\isanewline%
-pow{\isacharunderscore}nat\ {\isacharparenleft}Suc\ n{\isacharparenright}\ x\ {\isacharequal}\ x\ {\isasymotimes}\ pow{\isacharunderscore}nat\ n\ x}.
+ \isa{pow{\isaliteral{5F}{\isacharunderscore}}nat\ {\isadigit{0}}\ x\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C6F6E653E}{\isasymone}}\isasep\isanewline%
+pow{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\ x\ {\isaliteral{3D}{\isacharequal}}\ x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ pow{\isaliteral{5F}{\isacharunderscore}}nat\ n\ x}.
\noindent As you can see from this example, for local definitions
you may use any specification tool which works together with
@@ -828,7 +828,7 @@
functors that have a canonical interpretation as type classes.
There is also the possibility of other interpretations. For
example, \isa{list}s also form a monoid with \isa{append} and
- \isa{{\isacharbrackleft}{\isacharbrackright}} as operations, but it seems inappropriate to apply to
+ \isa{{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}} as operations, but it seems inappropriate to apply to
lists the same operations as for genuinely algebraic types. In such
a case, we can simply make a particular interpretation of monoids
for lists:%
@@ -841,7 +841,7 @@
%
\isatagquote
\isacommand{interpretation}\isamarkupfalse%
-\ list{\isacharunderscore}monoid{\isacharcolon}\ monoid\ append\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
+\ list{\isaliteral{5F}{\isacharunderscore}}monoid{\isaliteral{3A}{\isacharcolon}}\ monoid\ append\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ \isacommand{qed}\isamarkupfalse%
\ auto%
@@ -854,7 +854,7 @@
%
\begin{isamarkuptext}%
\noindent This enables us to apply facts on monoids
- to lists, e.g. \isa{{\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ x\ {\isacharequal}\ x}.
+ to lists, e.g. \isa{{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{40}{\isacharat}}\ x\ {\isaliteral{3D}{\isacharequal}}\ x}.
When using this interpretation pattern, it may also
be appropriate to map derived definitions accordingly:%
@@ -867,32 +867,32 @@
%
\isatagquote
\isacommand{primrec}\isamarkupfalse%
-\ replicate\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isasymalpha}\ list\ {\isasymRightarrow}\ {\isasymalpha}\ list{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-\ \ {\isachardoublequoteopen}replicate\ {\isadigit{0}}\ {\isacharunderscore}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
-\ \ {\isacharbar}\ {\isachardoublequoteopen}replicate\ {\isacharparenleft}Suc\ n{\isacharparenright}\ xs\ {\isacharequal}\ xs\ {\isacharat}\ replicate\ n\ xs{\isachardoublequoteclose}\isanewline
+\ replicate\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ list{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
+\ \ {\isaliteral{22}{\isachardoublequoteopen}}replicate\ {\isadigit{0}}\ {\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ \ {\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}replicate\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\ xs\ {\isaliteral{3D}{\isacharequal}}\ xs\ {\isaliteral{40}{\isacharat}}\ replicate\ n\ xs{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\isanewline
\isacommand{interpretation}\isamarkupfalse%
-\ list{\isacharunderscore}monoid{\isacharcolon}\ monoid\ append\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-\ \ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ append\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ replicate{\isachardoublequoteclose}\isanewline
+\ list{\isaliteral{5F}{\isacharunderscore}}monoid{\isaliteral{3A}{\isacharcolon}}\ monoid\ append\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
+\ \ {\isaliteral{22}{\isachardoublequoteopen}}monoid{\isaliteral{2E}{\isachardot}}pow{\isaliteral{5F}{\isacharunderscore}}nat\ append\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ replicate{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\isacommand{proof}\isamarkupfalse%
-\ {\isacharminus}\isanewline
+\ {\isaliteral{2D}{\isacharminus}}\isanewline
\ \ \isacommand{interpret}\isamarkupfalse%
-\ monoid\ append\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+\ monoid\ append\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
\isanewline
\ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ append\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ replicate{\isachardoublequoteclose}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}monoid{\isaliteral{2E}{\isachardot}}pow{\isaliteral{5F}{\isacharunderscore}}nat\ append\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ replicate{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{fix}\isamarkupfalse%
\ n\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ append\ {\isacharbrackleft}{\isacharbrackright}\ n\ {\isacharequal}\ replicate\ n{\isachardoublequoteclose}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}monoid{\isaliteral{2E}{\isachardot}}pow{\isaliteral{5F}{\isacharunderscore}}nat\ append\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ n\ {\isaliteral{3D}{\isacharequal}}\ replicate\ n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}induct\ n{\isacharparenright}\ auto\isanewline
+\ {\isaliteral{28}{\isacharparenleft}}induct\ n{\isaliteral{29}{\isacharparenright}}\ auto\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
-\ intro{\isacharunderscore}locales%
+\ intro{\isaliteral{5F}{\isacharunderscore}}locales%
\endisatagquote
{\isafoldquote}%
%
@@ -928,22 +928,22 @@
%
\isatagquote
\isacommand{subclass}\isamarkupfalse%
-\ {\isacharparenleft}\isakeyword{in}\ group{\isacharparenright}\ monoid\isanewline
+\ {\isaliteral{28}{\isacharparenleft}}\isakeyword{in}\ group{\isaliteral{29}{\isacharparenright}}\ monoid\isanewline
\isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
\ x\isanewline
\ \ \isacommand{from}\isamarkupfalse%
\ invl\ \isacommand{have}\isamarkupfalse%
-\ {\isachardoublequoteopen}x{\isasymdiv}\ {\isasymotimes}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}x{\isaliteral{5C3C6469763E}{\isasymdiv}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ x\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C6F6E653E}{\isasymone}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{with}\isamarkupfalse%
-\ assoc\ {\isacharbrackleft}symmetric{\isacharbrackright}\ neutl\ invl\ \isacommand{have}\isamarkupfalse%
-\ {\isachardoublequoteopen}x{\isasymdiv}\ {\isasymotimes}\ {\isacharparenleft}x\ {\isasymotimes}\ {\isasymone}{\isacharparenright}\ {\isacharequal}\ x{\isasymdiv}\ {\isasymotimes}\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
+\ assoc\ {\isaliteral{5B}{\isacharbrackleft}}symmetric{\isaliteral{5D}{\isacharbrackright}}\ neutl\ invl\ \isacommand{have}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}x{\isaliteral{5C3C6469763E}{\isasymdiv}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ {\isaliteral{5C3C6F6E653E}{\isasymone}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ x{\isaliteral{5C3C6469763E}{\isasymdiv}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{with}\isamarkupfalse%
-\ left{\isacharunderscore}cancel\ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}x\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
+\ left{\isaliteral{5F}{\isacharunderscore}}cancel\ \isacommand{show}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ {\isaliteral{5C3C6F6E653E}{\isasymone}}\ {\isaliteral{3D}{\isacharequal}}\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\isacommand{qed}\isamarkupfalse%
%
@@ -985,12 +985,12 @@
\end{picture}
\caption{Subclass relationship of monoids and groups:
before and after establishing the relationship
- \isa{group\ {\isasymsubseteq}\ monoid}; transitive edges are left out.}
+ \isa{group\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ monoid}; transitive edges are left out.}
\label{fig:subclass}
\end{center}
\end{figure}
- For illustration, a derived definition in \isa{group} using \isa{pow{\isacharunderscore}nat}%
+ For illustration, a derived definition in \isa{group} using \isa{pow{\isaliteral{5F}{\isacharunderscore}}nat}%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -1000,10 +1000,10 @@
%
\isatagquote
\isacommand{definition}\isamarkupfalse%
-\ {\isacharparenleft}\isakeyword{in}\ group{\isacharparenright}\ pow{\isacharunderscore}int\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}int\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-\ \ {\isachardoublequoteopen}pow{\isacharunderscore}int\ k\ x\ {\isacharequal}\ {\isacharparenleft}if\ k\ {\isachargreater}{\isacharequal}\ {\isadigit{0}}\isanewline
-\ \ \ \ then\ pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ k{\isacharparenright}\ x\isanewline
-\ \ \ \ else\ {\isacharparenleft}pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ {\isacharparenleft}{\isacharminus}\ k{\isacharparenright}{\isacharparenright}\ x{\isacharparenright}{\isasymdiv}{\isacharparenright}{\isachardoublequoteclose}%
+\ {\isaliteral{28}{\isacharparenleft}}\isakeyword{in}\ group{\isaliteral{29}{\isacharparenright}}\ pow{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}int\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
+\ \ {\isaliteral{22}{\isachardoublequoteopen}}pow{\isaliteral{5F}{\isacharunderscore}}int\ k\ x\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ k\ {\isaliteral{3E}{\isachargreater}}{\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}\isanewline
+\ \ \ \ then\ pow{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{28}{\isacharparenleft}}nat\ k{\isaliteral{29}{\isacharparenright}}\ x\isanewline
+\ \ \ \ else\ {\isaliteral{28}{\isacharparenleft}}pow{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{28}{\isacharparenleft}}nat\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2D}{\isacharminus}}\ k{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C6469763E}{\isasymdiv}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
\endisatagquote
{\isafoldquote}%
%
@@ -1012,7 +1012,7 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\noindent yields the global definition of \isa{{\isachardoublequote}pow{\isacharunderscore}int\ {\isasymColon}\ int\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group{\isachardoublequote}} with the corresponding theorem \isa{pow{\isacharunderscore}int\ k\ x\ {\isacharequal}\ {\isacharparenleft}if\ {\isadigit{0}}\ {\isasymle}\ k\ then\ pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ k{\isacharparenright}\ x\ else\ {\isacharparenleft}pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ {\isacharparenleft}{\isacharminus}\ k{\isacharparenright}{\isacharparenright}\ x{\isacharparenright}{\isasymdiv}{\isacharparenright}}.%
+\noindent yields the global definition of \isa{{\isaliteral{22}{\isachardoublequote}}pow{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}\ int\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}group\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}group{\isaliteral{22}{\isachardoublequote}}} with the corresponding theorem \isa{pow{\isaliteral{5F}{\isacharunderscore}}int\ k\ x\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ {\isadigit{0}}\ {\isaliteral{5C3C6C653E}{\isasymle}}\ k\ then\ pow{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{28}{\isacharparenleft}}nat\ k{\isaliteral{29}{\isacharparenright}}\ x\ else\ {\isaliteral{28}{\isacharparenleft}}pow{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{28}{\isacharparenleft}}nat\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2D}{\isacharminus}}\ k{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C6469763E}{\isasymdiv}}{\isaliteral{29}{\isacharparenright}}}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -1037,12 +1037,12 @@
\isakeyword{begin}\isanewline
\isanewline
\isacommand{term}\isamarkupfalse%
-\ {\isachardoublequoteopen}x\ {\isasymotimes}\ y{\isachardoublequoteclose}\ %
+\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ y{\isaliteral{22}{\isachardoublequoteclose}}\ %
\isamarkupcmt{example 1%
}
\isanewline
\isacommand{term}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isacharparenleft}x{\isasymColon}nat{\isacharparenright}\ {\isasymotimes}\ y{\isachardoublequoteclose}\ %
+\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}nat{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ y{\isaliteral{22}{\isachardoublequoteclose}}\ %
\isamarkupcmt{example 2%
}
\isanewline
@@ -1051,7 +1051,7 @@
\isanewline
\isanewline
\isacommand{term}\isamarkupfalse%
-\ {\isachardoublequoteopen}x\ {\isasymotimes}\ y{\isachardoublequoteclose}\ %
+\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ y{\isaliteral{22}{\isachardoublequoteclose}}\ %
\isamarkupcmt{example 3%
}
%
@@ -1064,10 +1064,10 @@
%
\begin{isamarkuptext}%
\noindent Here in example 1, the term refers to the local class
- operation \isa{mult\ {\isacharbrackleft}{\isasymalpha}{\isacharbrackright}}, whereas in example 2 the type
- constraint enforces the global class operation \isa{mult\ {\isacharbrackleft}nat{\isacharbrackright}}.
+ operation \isa{mult\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5D}{\isacharbrackright}}}, whereas in example 2 the type
+ constraint enforces the global class operation \isa{mult\ {\isaliteral{5B}{\isacharbrackleft}}nat{\isaliteral{5D}{\isacharbrackright}}}.
In the global context in example 3, the reference is to the
- polymorphic global class operation \isa{mult\ {\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isasymColon}\ semigroup{\isacharbrackright}}.%
+ polymorphic global class operation \isa{mult\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}\ semigroup{\isaliteral{5D}{\isacharbrackright}}}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -1096,8 +1096,8 @@
%
\isatagquote
\isacommand{definition}\isamarkupfalse%
-\ example\ {\isacharcolon}{\isacharcolon}\ int\ \isakeyword{where}\isanewline
-\ \ {\isachardoublequoteopen}example\ {\isacharequal}\ pow{\isacharunderscore}int\ {\isadigit{1}}{\isadigit{0}}\ {\isacharparenleft}{\isacharminus}{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}%
+\ example\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ int\ \isakeyword{where}\isanewline
+\ \ {\isaliteral{22}{\isachardoublequoteopen}}example\ {\isaliteral{3D}{\isacharequal}}\ pow{\isaliteral{5F}{\isacharunderscore}}int\ {\isadigit{1}}{\isadigit{0}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2D}{\isacharminus}}{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
\endisatagquote
{\isafoldquote}%
%
@@ -1130,68 +1130,68 @@
\isatagquotetypewriter
%
\begin{isamarkuptext}%
-module\ Example\ where\ {\isacharbraceleft}\isanewline
+module\ Example\ where\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
\isanewline
-data\ Nat\ {\isacharequal}\ Zero{\isacharunderscore}nat\ {\isacharbar}\ Suc\ Nat{\isacharsemicolon}\isanewline
+data\ Nat\ {\isaliteral{3D}{\isacharequal}}\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{7C}{\isacharbar}}\ Suc\ Nat{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\isanewline
-nat{\isacharunderscore}aux\ {\isacharcolon}{\isacharcolon}\ Integer\ {\isacharminus}{\isachargreater}\ Nat\ {\isacharminus}{\isachargreater}\ Nat{\isacharsemicolon}\isanewline
-nat{\isacharunderscore}aux\ i\ n\ {\isacharequal}\ {\isacharparenleft}if\ i\ {\isacharless}{\isacharequal}\ {\isadigit{0}}\ then\ n\ else\ nat{\isacharunderscore}aux\ {\isacharparenleft}i\ {\isacharminus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline
+nat{\isaliteral{5F}{\isacharunderscore}}aux\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ Integer\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ Nat\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ Nat{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+nat{\isaliteral{5F}{\isacharunderscore}}aux\ i\ n\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ i\ {\isaliteral{3C}{\isacharless}}{\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}\ then\ n\ else\ nat{\isaliteral{5F}{\isacharunderscore}}aux\ {\isaliteral{28}{\isacharparenleft}}i\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\isanewline
-nat\ {\isacharcolon}{\isacharcolon}\ Integer\ {\isacharminus}{\isachargreater}\ Nat{\isacharsemicolon}\isanewline
-nat\ i\ {\isacharequal}\ nat{\isacharunderscore}aux\ i\ Zero{\isacharunderscore}nat{\isacharsemicolon}\isanewline
+nat\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ Integer\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ Nat{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+nat\ i\ {\isaliteral{3D}{\isacharequal}}\ nat{\isaliteral{5F}{\isacharunderscore}}aux\ i\ Zero{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\isanewline
-class\ Semigroup\ a\ where\ {\isacharbraceleft}\isanewline
-\ \ mult\ {\isacharcolon}{\isacharcolon}\ a\ {\isacharminus}{\isachargreater}\ a\ {\isacharminus}{\isachargreater}\ a{\isacharsemicolon}\isanewline
-{\isacharbraceright}{\isacharsemicolon}\isanewline
+class\ Semigroup\ a\ where\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
+\ \ mult\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ a{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\isanewline
-class\ {\isacharparenleft}Semigroup\ a{\isacharparenright}\ {\isacharequal}{\isachargreater}\ Monoidl\ a\ where\ {\isacharbraceleft}\isanewline
-\ \ neutral\ {\isacharcolon}{\isacharcolon}\ a{\isacharsemicolon}\isanewline
-{\isacharbraceright}{\isacharsemicolon}\isanewline
+class\ {\isaliteral{28}{\isacharparenleft}}Semigroup\ a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ Monoidl\ a\ where\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
+\ \ neutral\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ a{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\isanewline
-class\ {\isacharparenleft}Monoidl\ a{\isacharparenright}\ {\isacharequal}{\isachargreater}\ Monoid\ a\ where\ {\isacharbraceleft}\isanewline
-{\isacharbraceright}{\isacharsemicolon}\isanewline
+class\ {\isaliteral{28}{\isacharparenleft}}Monoidl\ a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ Monoid\ a\ where\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
+{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\isanewline
-class\ {\isacharparenleft}Monoid\ a{\isacharparenright}\ {\isacharequal}{\isachargreater}\ Group\ a\ where\ {\isacharbraceleft}\isanewline
-\ \ inverse\ {\isacharcolon}{\isacharcolon}\ a\ {\isacharminus}{\isachargreater}\ a{\isacharsemicolon}\isanewline
-{\isacharbraceright}{\isacharsemicolon}\isanewline
+class\ {\isaliteral{28}{\isacharparenleft}}Monoid\ a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ Group\ a\ where\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
+\ \ inverse\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ a{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\isanewline
-pow{\isacharunderscore}nat\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ {\isacharparenleft}Monoid\ a{\isacharparenright}\ {\isacharequal}{\isachargreater}\ Nat\ {\isacharminus}{\isachargreater}\ a\ {\isacharminus}{\isachargreater}\ a{\isacharsemicolon}\isanewline
-pow{\isacharunderscore}nat\ Zero{\isacharunderscore}nat\ x\ {\isacharequal}\ neutral{\isacharsemicolon}\isanewline
-pow{\isacharunderscore}nat\ {\isacharparenleft}Suc\ n{\isacharparenright}\ x\ {\isacharequal}\ mult\ x\ {\isacharparenleft}pow{\isacharunderscore}nat\ n\ x{\isacharparenright}{\isacharsemicolon}\isanewline
+pow{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ forall\ a{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}Monoid\ a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ Nat\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ a{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+pow{\isaliteral{5F}{\isacharunderscore}}nat\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\ x\ {\isaliteral{3D}{\isacharequal}}\ neutral{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+pow{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\ x\ {\isaliteral{3D}{\isacharequal}}\ mult\ x\ {\isaliteral{28}{\isacharparenleft}}pow{\isaliteral{5F}{\isacharunderscore}}nat\ n\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\isanewline
-pow{\isacharunderscore}int\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ {\isacharparenleft}Group\ a{\isacharparenright}\ {\isacharequal}{\isachargreater}\ Integer\ {\isacharminus}{\isachargreater}\ a\ {\isacharminus}{\isachargreater}\ a{\isacharsemicolon}\isanewline
-pow{\isacharunderscore}int\ k\ x\ {\isacharequal}\isanewline
-\ \ {\isacharparenleft}if\ {\isadigit{0}}\ {\isacharless}{\isacharequal}\ k\ then\ pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ k{\isacharparenright}\ x\isanewline
-\ \ \ \ else\ inverse\ {\isacharparenleft}pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ {\isacharparenleft}negate\ k{\isacharparenright}{\isacharparenright}\ x{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline
+pow{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ forall\ a{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}Group\ a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ Integer\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ a{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+pow{\isaliteral{5F}{\isacharunderscore}}int\ k\ x\ {\isaliteral{3D}{\isacharequal}}\isanewline
+\ \ {\isaliteral{28}{\isacharparenleft}}if\ {\isadigit{0}}\ {\isaliteral{3C}{\isacharless}}{\isaliteral{3D}{\isacharequal}}\ k\ then\ pow{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{28}{\isacharparenleft}}nat\ k{\isaliteral{29}{\isacharparenright}}\ x\isanewline
+\ \ \ \ else\ inverse\ {\isaliteral{28}{\isacharparenleft}}pow{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{28}{\isacharparenleft}}nat\ {\isaliteral{28}{\isacharparenleft}}negate\ k{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\isanewline
-mult{\isacharunderscore}int\ {\isacharcolon}{\isacharcolon}\ Integer\ {\isacharminus}{\isachargreater}\ Integer\ {\isacharminus}{\isachargreater}\ Integer{\isacharsemicolon}\isanewline
-mult{\isacharunderscore}int\ i\ j\ {\isacharequal}\ i\ {\isacharplus}\ j{\isacharsemicolon}\isanewline
+mult{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ Integer\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ Integer\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ Integer{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+mult{\isaliteral{5F}{\isacharunderscore}}int\ i\ j\ {\isaliteral{3D}{\isacharequal}}\ i\ {\isaliteral{2B}{\isacharplus}}\ j{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\isanewline
-instance\ Semigroup\ Integer\ where\ {\isacharbraceleft}\isanewline
-\ \ mult\ {\isacharequal}\ mult{\isacharunderscore}int{\isacharsemicolon}\isanewline
-{\isacharbraceright}{\isacharsemicolon}\isanewline
+instance\ Semigroup\ Integer\ where\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
+\ \ mult\ {\isaliteral{3D}{\isacharequal}}\ mult{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\isanewline
-neutral{\isacharunderscore}int\ {\isacharcolon}{\isacharcolon}\ Integer{\isacharsemicolon}\isanewline
-neutral{\isacharunderscore}int\ {\isacharequal}\ {\isadigit{0}}{\isacharsemicolon}\isanewline
+neutral{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ Integer{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+neutral{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\isanewline
-instance\ Monoidl\ Integer\ where\ {\isacharbraceleft}\isanewline
-\ \ neutral\ {\isacharequal}\ neutral{\isacharunderscore}int{\isacharsemicolon}\isanewline
-{\isacharbraceright}{\isacharsemicolon}\isanewline
+instance\ Monoidl\ Integer\ where\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
+\ \ neutral\ {\isaliteral{3D}{\isacharequal}}\ neutral{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\isanewline
-instance\ Monoid\ Integer\ where\ {\isacharbraceleft}\isanewline
-{\isacharbraceright}{\isacharsemicolon}\isanewline
+instance\ Monoid\ Integer\ where\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
+{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\isanewline
-inverse{\isacharunderscore}int\ {\isacharcolon}{\isacharcolon}\ Integer\ {\isacharminus}{\isachargreater}\ Integer{\isacharsemicolon}\isanewline
-inverse{\isacharunderscore}int\ i\ {\isacharequal}\ negate\ i{\isacharsemicolon}\isanewline
+inverse{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ Integer\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ Integer{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+inverse{\isaliteral{5F}{\isacharunderscore}}int\ i\ {\isaliteral{3D}{\isacharequal}}\ negate\ i{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\isanewline
-instance\ Group\ Integer\ where\ {\isacharbraceleft}\isanewline
-\ \ inverse\ {\isacharequal}\ inverse{\isacharunderscore}int{\isacharsemicolon}\isanewline
-{\isacharbraceright}{\isacharsemicolon}\isanewline
+instance\ Group\ Integer\ where\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
+\ \ inverse\ {\isaliteral{3D}{\isacharequal}}\ inverse{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\isanewline
-example\ {\isacharcolon}{\isacharcolon}\ Integer{\isacharsemicolon}\isanewline
-example\ {\isacharequal}\ pow{\isacharunderscore}int\ {\isadigit{1}}{\isadigit{0}}\ {\isacharparenleft}{\isacharminus}{\isadigit{2}}{\isacharparenright}{\isacharsemicolon}\isanewline
+example\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ Integer{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+example\ {\isaliteral{3D}{\isacharequal}}\ pow{\isaliteral{5F}{\isacharunderscore}}int\ {\isadigit{1}}{\isadigit{0}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2D}{\isacharminus}}{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\isanewline
-{\isacharbraceright}\isanewline%
+{\isaliteral{7D}{\isacharbraceright}}\isanewline%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -1214,84 +1214,84 @@
\isatagquotetypewriter
%
\begin{isamarkuptext}%
-structure\ Example\ {\isacharcolon}\ sig\isanewline
-\ \ datatype\ nat\ {\isacharequal}\ Zero{\isacharunderscore}nat\ {\isacharbar}\ Suc\ of\ nat\isanewline
-\ \ val\ nat{\isacharunderscore}aux\ {\isacharcolon}\ IntInf{\isachardot}int\ {\isacharminus}{\isachargreater}\ nat\ {\isacharminus}{\isachargreater}\ nat\isanewline
-\ \ val\ nat\ {\isacharcolon}\ IntInf{\isachardot}int\ {\isacharminus}{\isachargreater}\ nat\isanewline
-\ \ type\ {\isacharprime}a\ semigroup\isanewline
-\ \ val\ mult\ {\isacharcolon}\ {\isacharprime}a\ semigroup\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\isanewline
-\ \ type\ {\isacharprime}a\ monoidl\isanewline
-\ \ val\ semigroup{\isacharunderscore}monoidl\ {\isacharcolon}\ {\isacharprime}a\ monoidl\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ semigroup\isanewline
-\ \ val\ neutral\ {\isacharcolon}\ {\isacharprime}a\ monoidl\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\isanewline
-\ \ type\ {\isacharprime}a\ monoid\isanewline
-\ \ val\ monoidl{\isacharunderscore}monoid\ {\isacharcolon}\ {\isacharprime}a\ monoid\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ monoidl\isanewline
-\ \ type\ {\isacharprime}a\ group\isanewline
-\ \ val\ monoid{\isacharunderscore}group\ {\isacharcolon}\ {\isacharprime}a\ group\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ monoid\isanewline
-\ \ val\ inverse\ {\isacharcolon}\ {\isacharprime}a\ group\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\isanewline
-\ \ val\ pow{\isacharunderscore}nat\ {\isacharcolon}\ {\isacharprime}a\ monoid\ {\isacharminus}{\isachargreater}\ nat\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\isanewline
-\ \ val\ pow{\isacharunderscore}int\ {\isacharcolon}\ {\isacharprime}a\ group\ {\isacharminus}{\isachargreater}\ IntInf{\isachardot}int\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\isanewline
-\ \ val\ mult{\isacharunderscore}int\ {\isacharcolon}\ IntInf{\isachardot}int\ {\isacharminus}{\isachargreater}\ IntInf{\isachardot}int\ {\isacharminus}{\isachargreater}\ IntInf{\isachardot}int\isanewline
-\ \ val\ semigroup{\isacharunderscore}int\ {\isacharcolon}\ IntInf{\isachardot}int\ semigroup\isanewline
-\ \ val\ neutral{\isacharunderscore}int\ {\isacharcolon}\ IntInf{\isachardot}int\isanewline
-\ \ val\ monoidl{\isacharunderscore}int\ {\isacharcolon}\ IntInf{\isachardot}int\ monoidl\isanewline
-\ \ val\ monoid{\isacharunderscore}int\ {\isacharcolon}\ IntInf{\isachardot}int\ monoid\isanewline
-\ \ val\ inverse{\isacharunderscore}int\ {\isacharcolon}\ IntInf{\isachardot}int\ {\isacharminus}{\isachargreater}\ IntInf{\isachardot}int\isanewline
-\ \ val\ group{\isacharunderscore}int\ {\isacharcolon}\ IntInf{\isachardot}int\ group\isanewline
-\ \ val\ example\ {\isacharcolon}\ IntInf{\isachardot}int\isanewline
-end\ {\isacharequal}\ struct\isanewline
+structure\ Example\ {\isaliteral{3A}{\isacharcolon}}\ sig\isanewline
+\ \ datatype\ nat\ {\isaliteral{3D}{\isacharequal}}\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{7C}{\isacharbar}}\ Suc\ of\ nat\isanewline
+\ \ val\ nat{\isaliteral{5F}{\isacharunderscore}}aux\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ nat\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ nat\isanewline
+\ \ val\ nat\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ nat\isanewline
+\ \ type\ {\isaliteral{27}{\isacharprime}}a\ semigroup\isanewline
+\ \ val\ mult\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ semigroup\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\isanewline
+\ \ type\ {\isaliteral{27}{\isacharprime}}a\ monoidl\isanewline
+\ \ val\ semigroup{\isaliteral{5F}{\isacharunderscore}}monoidl\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ monoidl\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ semigroup\isanewline
+\ \ val\ neutral\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ monoidl\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\isanewline
+\ \ type\ {\isaliteral{27}{\isacharprime}}a\ monoid\isanewline
+\ \ val\ monoidl{\isaliteral{5F}{\isacharunderscore}}monoid\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ monoid\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ monoidl\isanewline
+\ \ type\ {\isaliteral{27}{\isacharprime}}a\ group\isanewline
+\ \ val\ monoid{\isaliteral{5F}{\isacharunderscore}}group\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ group\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ monoid\isanewline
+\ \ val\ inverse\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ group\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\isanewline
+\ \ val\ pow{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ monoid\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ nat\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\isanewline
+\ \ val\ pow{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ group\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\isanewline
+\ \ val\ mult{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ IntInf{\isaliteral{2E}{\isachardot}}int\isanewline
+\ \ val\ semigroup{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ semigroup\isanewline
+\ \ val\ neutral{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\isanewline
+\ \ val\ monoidl{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ monoidl\isanewline
+\ \ val\ monoid{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ monoid\isanewline
+\ \ val\ inverse{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ IntInf{\isaliteral{2E}{\isachardot}}int\isanewline
+\ \ val\ group{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ group\isanewline
+\ \ val\ example\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\isanewline
+end\ {\isaliteral{3D}{\isacharequal}}\ struct\isanewline
\isanewline
-datatype\ nat\ {\isacharequal}\ Zero{\isacharunderscore}nat\ {\isacharbar}\ Suc\ of\ nat{\isacharsemicolon}\isanewline
+datatype\ nat\ {\isaliteral{3D}{\isacharequal}}\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{7C}{\isacharbar}}\ Suc\ of\ nat{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\isanewline
-fun\ nat{\isacharunderscore}aux\ i\ n\ {\isacharequal}\isanewline
-\ \ {\isacharparenleft}if\ IntInf{\isachardot}{\isacharless}{\isacharequal}\ {\isacharparenleft}i{\isacharcomma}\ {\isacharparenleft}{\isadigit{0}}\ {\isacharcolon}\ IntInf{\isachardot}int{\isacharparenright}{\isacharparenright}\ then\ n\isanewline
-\ \ \ \ else\ nat{\isacharunderscore}aux\ {\isacharparenleft}IntInf{\isachardot}{\isacharminus}\ {\isacharparenleft}i{\isacharcomma}\ {\isacharparenleft}{\isadigit{1}}\ {\isacharcolon}\ IntInf{\isachardot}int{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline
+fun\ nat{\isaliteral{5F}{\isacharunderscore}}aux\ i\ n\ {\isaliteral{3D}{\isacharequal}}\isanewline
+\ \ {\isaliteral{28}{\isacharparenleft}}if\ IntInf{\isaliteral{2E}{\isachardot}}{\isaliteral{3C}{\isacharless}}{\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}i{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ then\ n\isanewline
+\ \ \ \ else\ nat{\isaliteral{5F}{\isacharunderscore}}aux\ {\isaliteral{28}{\isacharparenleft}}IntInf{\isaliteral{2E}{\isachardot}}{\isaliteral{2D}{\isacharminus}}\ {\isaliteral{28}{\isacharparenleft}}i{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\isanewline
-fun\ nat\ i\ {\isacharequal}\ nat{\isacharunderscore}aux\ i\ Zero{\isacharunderscore}nat{\isacharsemicolon}\isanewline
+fun\ nat\ i\ {\isaliteral{3D}{\isacharequal}}\ nat{\isaliteral{5F}{\isacharunderscore}}aux\ i\ Zero{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\isanewline
-type\ {\isacharprime}a\ semigroup\ {\isacharequal}\ {\isacharbraceleft}mult\ {\isacharcolon}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a{\isacharbraceright}{\isacharsemicolon}\isanewline
-val\ mult\ {\isacharequal}\ {\isacharhash}mult\ {\isacharcolon}\ {\isacharprime}a\ semigroup\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a{\isacharsemicolon}\isanewline
+type\ {\isaliteral{27}{\isacharprime}}a\ semigroup\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}mult\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+val\ mult\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{23}{\isacharhash}}mult\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ semigroup\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\isanewline
-type\ {\isacharprime}a\ monoidl\ {\isacharequal}\ {\isacharbraceleft}semigroup{\isacharunderscore}monoidl\ {\isacharcolon}\ {\isacharprime}a\ semigroup{\isacharcomma}\ neutral\ {\isacharcolon}\ {\isacharprime}a{\isacharbraceright}{\isacharsemicolon}\isanewline
-val\ semigroup{\isacharunderscore}monoidl\ {\isacharequal}\ {\isacharhash}semigroup{\isacharunderscore}monoidl\ {\isacharcolon}\ {\isacharprime}a\ monoidl\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ semigroup{\isacharsemicolon}\isanewline
-val\ neutral\ {\isacharequal}\ {\isacharhash}neutral\ {\isacharcolon}\ {\isacharprime}a\ monoidl\ {\isacharminus}{\isachargreater}\ {\isacharprime}a{\isacharsemicolon}\isanewline
+type\ {\isaliteral{27}{\isacharprime}}a\ monoidl\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}semigroup{\isaliteral{5F}{\isacharunderscore}}monoidl\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ semigroup{\isaliteral{2C}{\isacharcomma}}\ neutral\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+val\ semigroup{\isaliteral{5F}{\isacharunderscore}}monoidl\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{23}{\isacharhash}}semigroup{\isaliteral{5F}{\isacharunderscore}}monoidl\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ monoidl\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ semigroup{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+val\ neutral\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{23}{\isacharhash}}neutral\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ monoidl\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\isanewline
-type\ {\isacharprime}a\ monoid\ {\isacharequal}\ {\isacharbraceleft}monoidl{\isacharunderscore}monoid\ {\isacharcolon}\ {\isacharprime}a\ monoidl{\isacharbraceright}{\isacharsemicolon}\isanewline
-val\ monoidl{\isacharunderscore}monoid\ {\isacharequal}\ {\isacharhash}monoidl{\isacharunderscore}monoid\ {\isacharcolon}\ {\isacharprime}a\ monoid\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ monoidl{\isacharsemicolon}\isanewline
+type\ {\isaliteral{27}{\isacharprime}}a\ monoid\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}monoidl{\isaliteral{5F}{\isacharunderscore}}monoid\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ monoidl{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+val\ monoidl{\isaliteral{5F}{\isacharunderscore}}monoid\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{23}{\isacharhash}}monoidl{\isaliteral{5F}{\isacharunderscore}}monoid\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ monoid\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ monoidl{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\isanewline
-type\ {\isacharprime}a\ group\ {\isacharequal}\ {\isacharbraceleft}monoid{\isacharunderscore}group\ {\isacharcolon}\ {\isacharprime}a\ monoid{\isacharcomma}\ inverse\ {\isacharcolon}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a{\isacharbraceright}{\isacharsemicolon}\isanewline
-val\ monoid{\isacharunderscore}group\ {\isacharequal}\ {\isacharhash}monoid{\isacharunderscore}group\ {\isacharcolon}\ {\isacharprime}a\ group\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ monoid{\isacharsemicolon}\isanewline
-val\ inverse\ {\isacharequal}\ {\isacharhash}inverse\ {\isacharcolon}\ {\isacharprime}a\ group\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a{\isacharsemicolon}\isanewline
+type\ {\isaliteral{27}{\isacharprime}}a\ group\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}monoid{\isaliteral{5F}{\isacharunderscore}}group\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ monoid{\isaliteral{2C}{\isacharcomma}}\ inverse\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+val\ monoid{\isaliteral{5F}{\isacharunderscore}}group\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{23}{\isacharhash}}monoid{\isaliteral{5F}{\isacharunderscore}}group\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ group\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ monoid{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+val\ inverse\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{23}{\isacharhash}}inverse\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ group\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\isanewline
-fun\ pow{\isacharunderscore}nat\ A{\isacharunderscore}\ Zero{\isacharunderscore}nat\ x\ {\isacharequal}\ neutral\ {\isacharparenleft}monoidl{\isacharunderscore}monoid\ A{\isacharunderscore}{\isacharparenright}\isanewline
-\ \ {\isacharbar}\ pow{\isacharunderscore}nat\ A{\isacharunderscore}\ {\isacharparenleft}Suc\ n{\isacharparenright}\ x\ {\isacharequal}\isanewline
-\ \ \ \ mult\ {\isacharparenleft}{\isacharparenleft}semigroup{\isacharunderscore}monoidl\ o\ monoidl{\isacharunderscore}monoid{\isacharparenright}\ A{\isacharunderscore}{\isacharparenright}\ x\ {\isacharparenleft}pow{\isacharunderscore}nat\ A{\isacharunderscore}\ n\ x{\isacharparenright}{\isacharsemicolon}\isanewline
+fun\ pow{\isaliteral{5F}{\isacharunderscore}}nat\ A{\isaliteral{5F}{\isacharunderscore}}\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\ x\ {\isaliteral{3D}{\isacharequal}}\ neutral\ {\isaliteral{28}{\isacharparenleft}}monoidl{\isaliteral{5F}{\isacharunderscore}}monoid\ A{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\isanewline
+\ \ {\isaliteral{7C}{\isacharbar}}\ pow{\isaliteral{5F}{\isacharunderscore}}nat\ A{\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\ x\ {\isaliteral{3D}{\isacharequal}}\isanewline
+\ \ \ \ mult\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}semigroup{\isaliteral{5F}{\isacharunderscore}}monoidl\ o\ monoidl{\isaliteral{5F}{\isacharunderscore}}monoid{\isaliteral{29}{\isacharparenright}}\ A{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ x\ {\isaliteral{28}{\isacharparenleft}}pow{\isaliteral{5F}{\isacharunderscore}}nat\ A{\isaliteral{5F}{\isacharunderscore}}\ n\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\isanewline
-fun\ pow{\isacharunderscore}int\ A{\isacharunderscore}\ k\ x\ {\isacharequal}\isanewline
-\ \ {\isacharparenleft}if\ IntInf{\isachardot}{\isacharless}{\isacharequal}\ {\isacharparenleft}{\isacharparenleft}{\isadigit{0}}\ {\isacharcolon}\ IntInf{\isachardot}int{\isacharparenright}{\isacharcomma}\ k{\isacharparenright}\isanewline
-\ \ \ \ then\ pow{\isacharunderscore}nat\ {\isacharparenleft}monoid{\isacharunderscore}group\ A{\isacharunderscore}{\isacharparenright}\ {\isacharparenleft}nat\ k{\isacharparenright}\ x\isanewline
-\ \ \ \ else\ inverse\ A{\isacharunderscore}\ {\isacharparenleft}pow{\isacharunderscore}nat\ {\isacharparenleft}monoid{\isacharunderscore}group\ A{\isacharunderscore}{\isacharparenright}\ {\isacharparenleft}nat\ {\isacharparenleft}IntInf{\isachardot}{\isachartilde}\ k{\isacharparenright}{\isacharparenright}\ x{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline
+fun\ pow{\isaliteral{5F}{\isacharunderscore}}int\ A{\isaliteral{5F}{\isacharunderscore}}\ k\ x\ {\isaliteral{3D}{\isacharequal}}\isanewline
+\ \ {\isaliteral{28}{\isacharparenleft}}if\ IntInf{\isaliteral{2E}{\isachardot}}{\isaliteral{3C}{\isacharless}}{\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ k{\isaliteral{29}{\isacharparenright}}\isanewline
+\ \ \ \ then\ pow{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{28}{\isacharparenleft}}monoid{\isaliteral{5F}{\isacharunderscore}}group\ A{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}nat\ k{\isaliteral{29}{\isacharparenright}}\ x\isanewline
+\ \ \ \ else\ inverse\ A{\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{28}{\isacharparenleft}}pow{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{28}{\isacharparenleft}}monoid{\isaliteral{5F}{\isacharunderscore}}group\ A{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}nat\ {\isaliteral{28}{\isacharparenleft}}IntInf{\isaliteral{2E}{\isachardot}}{\isaliteral{7E}{\isachartilde}}\ k{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\isanewline
-fun\ mult{\isacharunderscore}int\ i\ j\ {\isacharequal}\ IntInf{\isachardot}{\isacharplus}\ {\isacharparenleft}i{\isacharcomma}\ j{\isacharparenright}{\isacharsemicolon}\isanewline
+fun\ mult{\isaliteral{5F}{\isacharunderscore}}int\ i\ j\ {\isaliteral{3D}{\isacharequal}}\ IntInf{\isaliteral{2E}{\isachardot}}{\isaliteral{2B}{\isacharplus}}\ {\isaliteral{28}{\isacharparenleft}}i{\isaliteral{2C}{\isacharcomma}}\ j{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\isanewline
-val\ semigroup{\isacharunderscore}int\ {\isacharequal}\ {\isacharbraceleft}mult\ {\isacharequal}\ mult{\isacharunderscore}int{\isacharbraceright}\ {\isacharcolon}\ IntInf{\isachardot}int\ semigroup{\isacharsemicolon}\isanewline
+val\ semigroup{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}mult\ {\isaliteral{3D}{\isacharequal}}\ mult{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ semigroup{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\isanewline
-val\ neutral{\isacharunderscore}int\ {\isacharcolon}\ IntInf{\isachardot}int\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}\ {\isacharcolon}\ IntInf{\isachardot}int{\isacharparenright}{\isacharsemicolon}\isanewline
+val\ neutral{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\isanewline
-val\ monoidl{\isacharunderscore}int\ {\isacharequal}\isanewline
-\ \ {\isacharbraceleft}semigroup{\isacharunderscore}monoidl\ {\isacharequal}\ semigroup{\isacharunderscore}int{\isacharcomma}\ neutral\ {\isacharequal}\ neutral{\isacharunderscore}int{\isacharbraceright}\ {\isacharcolon}\isanewline
-\ \ IntInf{\isachardot}int\ monoidl{\isacharsemicolon}\isanewline
+val\ monoidl{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3D}{\isacharequal}}\isanewline
+\ \ {\isaliteral{7B}{\isacharbraceleft}}semigroup{\isaliteral{5F}{\isacharunderscore}}monoidl\ {\isaliteral{3D}{\isacharequal}}\ semigroup{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{2C}{\isacharcomma}}\ neutral\ {\isaliteral{3D}{\isacharequal}}\ neutral{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{3A}{\isacharcolon}}\isanewline
+\ \ IntInf{\isaliteral{2E}{\isachardot}}int\ monoidl{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\isanewline
-val\ monoid{\isacharunderscore}int\ {\isacharequal}\ {\isacharbraceleft}monoidl{\isacharunderscore}monoid\ {\isacharequal}\ monoidl{\isacharunderscore}int{\isacharbraceright}\ {\isacharcolon}\ IntInf{\isachardot}int\ monoid{\isacharsemicolon}\isanewline
+val\ monoid{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}monoidl{\isaliteral{5F}{\isacharunderscore}}monoid\ {\isaliteral{3D}{\isacharequal}}\ monoidl{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ monoid{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\isanewline
-fun\ inverse{\isacharunderscore}int\ i\ {\isacharequal}\ IntInf{\isachardot}{\isachartilde}\ i{\isacharsemicolon}\isanewline
+fun\ inverse{\isaliteral{5F}{\isacharunderscore}}int\ i\ {\isaliteral{3D}{\isacharequal}}\ IntInf{\isaliteral{2E}{\isachardot}}{\isaliteral{7E}{\isachartilde}}\ i{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\isanewline
-val\ group{\isacharunderscore}int\ {\isacharequal}\ {\isacharbraceleft}monoid{\isacharunderscore}group\ {\isacharequal}\ monoid{\isacharunderscore}int{\isacharcomma}\ inverse\ {\isacharequal}\ inverse{\isacharunderscore}int{\isacharbraceright}\ {\isacharcolon}\isanewline
-\ \ IntInf{\isachardot}int\ group{\isacharsemicolon}\isanewline
+val\ group{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}monoid{\isaliteral{5F}{\isacharunderscore}}group\ {\isaliteral{3D}{\isacharequal}}\ monoid{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{2C}{\isacharcomma}}\ inverse\ {\isaliteral{3D}{\isacharequal}}\ inverse{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{3A}{\isacharcolon}}\isanewline
+\ \ IntInf{\isaliteral{2E}{\isachardot}}int\ group{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\isanewline
-val\ example\ {\isacharcolon}\ IntInf{\isachardot}int\ {\isacharequal}\isanewline
-\ \ pow{\isacharunderscore}int\ group{\isacharunderscore}int\ {\isacharparenleft}{\isadigit{1}}{\isadigit{0}}\ {\isacharcolon}\ IntInf{\isachardot}int{\isacharparenright}\ {\isacharparenleft}{\isachartilde}{\isadigit{2}}\ {\isacharcolon}\ IntInf{\isachardot}int{\isacharparenright}{\isacharsemicolon}\isanewline
+val\ example\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ {\isaliteral{3D}{\isacharequal}}\isanewline
+\ \ pow{\isaliteral{5F}{\isacharunderscore}}int\ group{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isadigit{0}}\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{7E}{\isachartilde}}{\isadigit{2}}\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\isanewline
-end{\isacharsemicolon}\ {\isacharparenleft}{\isacharasterisk}struct\ Example{\isacharasterisk}{\isacharparenright}\isanewline%
+end{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}struct\ Example{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -1327,74 +1327,74 @@
\isatagquotetypewriter
%
\begin{isamarkuptext}%
-object\ Example\ {\isacharbraceleft}\isanewline
+object\ Example\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
\isanewline
abstract\ sealed\ class\ nat\isanewline
-final\ case\ object\ Zero{\isacharunderscore}nat\ extends\ nat\isanewline
-final\ case\ class\ Suc{\isacharparenleft}a{\isacharcolon}\ nat{\isacharparenright}\ extends\ nat\isanewline
+final\ case\ object\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\ extends\ nat\isanewline
+final\ case\ class\ Suc{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{3A}{\isacharcolon}}\ nat{\isaliteral{29}{\isacharparenright}}\ extends\ nat\isanewline
\isanewline
-def\ nat{\isacharunderscore}aux{\isacharparenleft}i{\isacharcolon}\ BigInt{\isacharcomma}\ n{\isacharcolon}\ nat{\isacharparenright}{\isacharcolon}\ nat\ {\isacharequal}\isanewline
-\ \ {\isacharparenleft}if\ {\isacharparenleft}i\ {\isacharless}{\isacharequal}\ BigInt{\isacharparenleft}{\isadigit{0}}{\isacharparenright}{\isacharparenright}\ n\ else\ nat{\isacharunderscore}aux{\isacharparenleft}i\ {\isacharminus}\ BigInt{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isacharcomma}\ Suc{\isacharparenleft}n{\isacharparenright}{\isacharparenright}{\isacharparenright}\isanewline
+def\ nat{\isaliteral{5F}{\isacharunderscore}}aux{\isaliteral{28}{\isacharparenleft}}i{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{2C}{\isacharcomma}}\ n{\isaliteral{3A}{\isacharcolon}}\ nat{\isaliteral{29}{\isacharparenright}}{\isaliteral{3A}{\isacharcolon}}\ nat\ {\isaliteral{3D}{\isacharequal}}\isanewline
+\ \ {\isaliteral{28}{\isacharparenleft}}if\ {\isaliteral{28}{\isacharparenleft}}i\ {\isaliteral{3C}{\isacharless}}{\isaliteral{3D}{\isacharequal}}\ BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ n\ else\ nat{\isaliteral{5F}{\isacharunderscore}}aux{\isaliteral{28}{\isacharparenleft}}i\ {\isaliteral{2D}{\isacharminus}}\ BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ Suc{\isaliteral{28}{\isacharparenleft}}n{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline
\isanewline
-def\ nat{\isacharparenleft}i{\isacharcolon}\ BigInt{\isacharparenright}{\isacharcolon}\ nat\ {\isacharequal}\ nat{\isacharunderscore}aux{\isacharparenleft}i{\isacharcomma}\ Zero{\isacharunderscore}nat{\isacharparenright}\isanewline
+def\ nat{\isaliteral{28}{\isacharparenleft}}i{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{29}{\isacharparenright}}{\isaliteral{3A}{\isacharcolon}}\ nat\ {\isaliteral{3D}{\isacharequal}}\ nat{\isaliteral{5F}{\isacharunderscore}}aux{\isaliteral{28}{\isacharparenleft}}i{\isaliteral{2C}{\isacharcomma}}\ Zero{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{29}{\isacharparenright}}\isanewline
\isanewline
-trait\ semigroup{\isacharbrackleft}A{\isacharbrackright}\ {\isacharbraceleft}\isanewline
-\ \ val\ {\isacharbackquote}Example{\isachardot}mult{\isacharbackquote}{\isacharcolon}\ {\isacharparenleft}A{\isacharcomma}\ A{\isacharparenright}\ {\isacharequal}{\isachargreater}\ A\isanewline
-{\isacharbraceright}\isanewline
-def\ mult{\isacharbrackleft}A{\isacharbrackright}{\isacharparenleft}a{\isacharcolon}\ A{\isacharcomma}\ b{\isacharcolon}\ A{\isacharparenright}{\isacharparenleft}implicit\ A{\isacharcolon}\ semigroup{\isacharbrackleft}A{\isacharbrackright}{\isacharparenright}{\isacharcolon}\ A\ {\isacharequal}\isanewline
-\ \ A{\isachardot}{\isacharbackquote}Example{\isachardot}mult{\isacharbackquote}{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\isanewline
+trait\ semigroup{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
+\ \ val\ {\isaliteral{60}{\isacharbackquote}}Example{\isaliteral{2E}{\isachardot}}mult{\isaliteral{60}{\isacharbackquote}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}A{\isaliteral{2C}{\isacharcomma}}\ A{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ A\isanewline
+{\isaliteral{7D}{\isacharbraceright}}\isanewline
+def\ mult{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{3A}{\isacharcolon}}\ A{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{3A}{\isacharcolon}}\ A{\isaliteral{29}{\isacharparenright}}{\isaliteral{28}{\isacharparenleft}}implicit\ A{\isaliteral{3A}{\isacharcolon}}\ semigroup{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3A}{\isacharcolon}}\ A\ {\isaliteral{3D}{\isacharequal}}\isanewline
+\ \ A{\isaliteral{2E}{\isachardot}}{\isaliteral{60}{\isacharbackquote}}Example{\isaliteral{2E}{\isachardot}}mult{\isaliteral{60}{\isacharbackquote}}{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{29}{\isacharparenright}}\isanewline
\isanewline
-trait\ monoidl{\isacharbrackleft}A{\isacharbrackright}\ extends\ semigroup{\isacharbrackleft}A{\isacharbrackright}\ {\isacharbraceleft}\isanewline
-\ \ val\ {\isacharbackquote}Example{\isachardot}neutral{\isacharbackquote}{\isacharcolon}\ A\isanewline
-{\isacharbraceright}\isanewline
-def\ neutral{\isacharbrackleft}A{\isacharbrackright}{\isacharparenleft}implicit\ A{\isacharcolon}\ monoidl{\isacharbrackleft}A{\isacharbrackright}{\isacharparenright}{\isacharcolon}\ A\ {\isacharequal}\ A{\isachardot}{\isacharbackquote}Example{\isachardot}neutral{\isacharbackquote}\isanewline
+trait\ monoidl{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}\ extends\ semigroup{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
+\ \ val\ {\isaliteral{60}{\isacharbackquote}}Example{\isaliteral{2E}{\isachardot}}neutral{\isaliteral{60}{\isacharbackquote}}{\isaliteral{3A}{\isacharcolon}}\ A\isanewline
+{\isaliteral{7D}{\isacharbraceright}}\isanewline
+def\ neutral{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{28}{\isacharparenleft}}implicit\ A{\isaliteral{3A}{\isacharcolon}}\ monoidl{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3A}{\isacharcolon}}\ A\ {\isaliteral{3D}{\isacharequal}}\ A{\isaliteral{2E}{\isachardot}}{\isaliteral{60}{\isacharbackquote}}Example{\isaliteral{2E}{\isachardot}}neutral{\isaliteral{60}{\isacharbackquote}}\isanewline
\isanewline
-trait\ monoid{\isacharbrackleft}A{\isacharbrackright}\ extends\ monoidl{\isacharbrackleft}A{\isacharbrackright}\ {\isacharbraceleft}\isanewline
-{\isacharbraceright}\isanewline
+trait\ monoid{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}\ extends\ monoidl{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
+{\isaliteral{7D}{\isacharbraceright}}\isanewline
\isanewline
-trait\ group{\isacharbrackleft}A{\isacharbrackright}\ extends\ monoid{\isacharbrackleft}A{\isacharbrackright}\ {\isacharbraceleft}\isanewline
-\ \ val\ {\isacharbackquote}Example{\isachardot}inverse{\isacharbackquote}{\isacharcolon}\ A\ {\isacharequal}{\isachargreater}\ A\isanewline
-{\isacharbraceright}\isanewline
-def\ inverse{\isacharbrackleft}A{\isacharbrackright}{\isacharparenleft}a{\isacharcolon}\ A{\isacharparenright}{\isacharparenleft}implicit\ A{\isacharcolon}\ group{\isacharbrackleft}A{\isacharbrackright}{\isacharparenright}{\isacharcolon}\ A\ {\isacharequal}\ A{\isachardot}{\isacharbackquote}Example{\isachardot}inverse{\isacharbackquote}{\isacharparenleft}a{\isacharparenright}\isanewline
+trait\ group{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}\ extends\ monoid{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
+\ \ val\ {\isaliteral{60}{\isacharbackquote}}Example{\isaliteral{2E}{\isachardot}}inverse{\isaliteral{60}{\isacharbackquote}}{\isaliteral{3A}{\isacharcolon}}\ A\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ A\isanewline
+{\isaliteral{7D}{\isacharbraceright}}\isanewline
+def\ inverse{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{3A}{\isacharcolon}}\ A{\isaliteral{29}{\isacharparenright}}{\isaliteral{28}{\isacharparenleft}}implicit\ A{\isaliteral{3A}{\isacharcolon}}\ group{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3A}{\isacharcolon}}\ A\ {\isaliteral{3D}{\isacharequal}}\ A{\isaliteral{2E}{\isachardot}}{\isaliteral{60}{\isacharbackquote}}Example{\isaliteral{2E}{\isachardot}}inverse{\isaliteral{60}{\isacharbackquote}}{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{29}{\isacharparenright}}\isanewline
\isanewline
-def\ pow{\isacharunderscore}nat{\isacharbrackleft}A{\isacharcolon}\ monoid{\isacharbrackright}{\isacharparenleft}xa{\isadigit{0}}{\isacharcolon}\ nat{\isacharcomma}\ x{\isacharcolon}\ A{\isacharparenright}{\isacharcolon}\ A\ {\isacharequal}\ {\isacharparenleft}xa{\isadigit{0}}{\isacharcomma}\ x{\isacharparenright}\ match\ {\isacharbraceleft}\isanewline
-\ \ case\ {\isacharparenleft}Zero{\isacharunderscore}nat{\isacharcomma}\ x{\isacharparenright}\ {\isacharequal}{\isachargreater}\ neutral{\isacharbrackleft}A{\isacharbrackright}\isanewline
-\ \ case\ {\isacharparenleft}Suc{\isacharparenleft}n{\isacharparenright}{\isacharcomma}\ x{\isacharparenright}\ {\isacharequal}{\isachargreater}\ mult{\isacharbrackleft}A{\isacharbrackright}{\isacharparenleft}x{\isacharcomma}\ pow{\isacharunderscore}nat{\isacharbrackleft}A{\isacharbrackright}{\isacharparenleft}n{\isacharcomma}\ x{\isacharparenright}{\isacharparenright}\isanewline
-{\isacharbraceright}\isanewline
+def\ pow{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{3A}{\isacharcolon}}\ monoid{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{28}{\isacharparenleft}}xa{\isadigit{0}}{\isaliteral{3A}{\isacharcolon}}\ nat{\isaliteral{2C}{\isacharcomma}}\ x{\isaliteral{3A}{\isacharcolon}}\ A{\isaliteral{29}{\isacharparenright}}{\isaliteral{3A}{\isacharcolon}}\ A\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}xa{\isadigit{0}}{\isaliteral{2C}{\isacharcomma}}\ x{\isaliteral{29}{\isacharparenright}}\ match\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
+\ \ case\ {\isaliteral{28}{\isacharparenleft}}Zero{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{2C}{\isacharcomma}}\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ neutral{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}\isanewline
+\ \ case\ {\isaliteral{28}{\isacharparenleft}}Suc{\isaliteral{28}{\isacharparenleft}}n{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ mult{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ pow{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{28}{\isacharparenleft}}n{\isaliteral{2C}{\isacharcomma}}\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline
+{\isaliteral{7D}{\isacharbraceright}}\isanewline
\isanewline
-def\ pow{\isacharunderscore}int{\isacharbrackleft}A{\isacharcolon}\ group{\isacharbrackright}{\isacharparenleft}k{\isacharcolon}\ BigInt{\isacharcomma}\ x{\isacharcolon}\ A{\isacharparenright}{\isacharcolon}\ A\ {\isacharequal}\isanewline
-\ \ {\isacharparenleft}if\ {\isacharparenleft}BigInt{\isacharparenleft}{\isadigit{0}}{\isacharparenright}\ {\isacharless}{\isacharequal}\ k{\isacharparenright}\ pow{\isacharunderscore}nat{\isacharbrackleft}A{\isacharbrackright}{\isacharparenleft}nat{\isacharparenleft}k{\isacharparenright}{\isacharcomma}\ x{\isacharparenright}\isanewline
-\ \ \ \ else\ inverse{\isacharbrackleft}A{\isacharbrackright}{\isacharparenleft}pow{\isacharunderscore}nat{\isacharbrackleft}A{\isacharbrackright}{\isacharparenleft}nat{\isacharparenleft}{\isacharparenleft}{\isacharminus}\ k{\isacharparenright}{\isacharparenright}{\isacharcomma}\ x{\isacharparenright}{\isacharparenright}{\isacharparenright}\isanewline
+def\ pow{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{3A}{\isacharcolon}}\ group{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{28}{\isacharparenleft}}k{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{2C}{\isacharcomma}}\ x{\isaliteral{3A}{\isacharcolon}}\ A{\isaliteral{29}{\isacharparenright}}{\isaliteral{3A}{\isacharcolon}}\ A\ {\isaliteral{3D}{\isacharequal}}\isanewline
+\ \ {\isaliteral{28}{\isacharparenleft}}if\ {\isaliteral{28}{\isacharparenleft}}BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3C}{\isacharless}}{\isaliteral{3D}{\isacharequal}}\ k{\isaliteral{29}{\isacharparenright}}\ pow{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{28}{\isacharparenleft}}nat{\isaliteral{28}{\isacharparenleft}}k{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ x{\isaliteral{29}{\isacharparenright}}\isanewline
+\ \ \ \ else\ inverse{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{28}{\isacharparenleft}}pow{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{28}{\isacharparenleft}}nat{\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2D}{\isacharminus}}\ k{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline
\isanewline
-def\ mult{\isacharunderscore}int{\isacharparenleft}i{\isacharcolon}\ BigInt{\isacharcomma}\ j{\isacharcolon}\ BigInt{\isacharparenright}{\isacharcolon}\ BigInt\ {\isacharequal}\ i\ {\isacharplus}\ j\isanewline
+def\ mult{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{28}{\isacharparenleft}}i{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{2C}{\isacharcomma}}\ j{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{29}{\isacharparenright}}{\isaliteral{3A}{\isacharcolon}}\ BigInt\ {\isaliteral{3D}{\isacharequal}}\ i\ {\isaliteral{2B}{\isacharplus}}\ j\isanewline
\isanewline
-implicit\ def\ semigroup{\isacharunderscore}int{\isacharcolon}\ semigroup{\isacharbrackleft}BigInt{\isacharbrackright}\ {\isacharequal}\ new\ semigroup{\isacharbrackleft}BigInt{\isacharbrackright}\ {\isacharbraceleft}\isanewline
-\ \ val\ {\isacharbackquote}Example{\isachardot}mult{\isacharbackquote}\ {\isacharequal}\ {\isacharparenleft}a{\isacharcolon}\ BigInt{\isacharcomma}\ b{\isacharcolon}\ BigInt{\isacharparenright}\ {\isacharequal}{\isachargreater}\ mult{\isacharunderscore}int{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\isanewline
-{\isacharbraceright}\isanewline
+implicit\ def\ semigroup{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{3A}{\isacharcolon}}\ semigroup{\isaliteral{5B}{\isacharbrackleft}}BigInt{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ new\ semigroup{\isaliteral{5B}{\isacharbrackleft}}BigInt{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
+\ \ val\ {\isaliteral{60}{\isacharbackquote}}Example{\isaliteral{2E}{\isachardot}}mult{\isaliteral{60}{\isacharbackquote}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ mult{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{29}{\isacharparenright}}\isanewline
+{\isaliteral{7D}{\isacharbraceright}}\isanewline
\isanewline
-def\ neutral{\isacharunderscore}int{\isacharcolon}\ BigInt\ {\isacharequal}\ BigInt{\isacharparenleft}{\isadigit{0}}{\isacharparenright}\isanewline
+def\ neutral{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{3A}{\isacharcolon}}\ BigInt\ {\isaliteral{3D}{\isacharequal}}\ BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline
\isanewline
-implicit\ def\ monoidl{\isacharunderscore}int{\isacharcolon}\ monoidl{\isacharbrackleft}BigInt{\isacharbrackright}\ {\isacharequal}\ new\ monoidl{\isacharbrackleft}BigInt{\isacharbrackright}\ {\isacharbraceleft}\isanewline
-\ \ val\ {\isacharbackquote}Example{\isachardot}neutral{\isacharbackquote}\ {\isacharequal}\ neutral{\isacharunderscore}int\isanewline
-\ \ val\ {\isacharbackquote}Example{\isachardot}mult{\isacharbackquote}\ {\isacharequal}\ {\isacharparenleft}a{\isacharcolon}\ BigInt{\isacharcomma}\ b{\isacharcolon}\ BigInt{\isacharparenright}\ {\isacharequal}{\isachargreater}\ mult{\isacharunderscore}int{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\isanewline
-{\isacharbraceright}\isanewline
+implicit\ def\ monoidl{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{3A}{\isacharcolon}}\ monoidl{\isaliteral{5B}{\isacharbrackleft}}BigInt{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ new\ monoidl{\isaliteral{5B}{\isacharbrackleft}}BigInt{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
+\ \ val\ {\isaliteral{60}{\isacharbackquote}}Example{\isaliteral{2E}{\isachardot}}neutral{\isaliteral{60}{\isacharbackquote}}\ {\isaliteral{3D}{\isacharequal}}\ neutral{\isaliteral{5F}{\isacharunderscore}}int\isanewline
+\ \ val\ {\isaliteral{60}{\isacharbackquote}}Example{\isaliteral{2E}{\isachardot}}mult{\isaliteral{60}{\isacharbackquote}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ mult{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{29}{\isacharparenright}}\isanewline
+{\isaliteral{7D}{\isacharbraceright}}\isanewline
\isanewline
-implicit\ def\ monoid{\isacharunderscore}int{\isacharcolon}\ monoid{\isacharbrackleft}BigInt{\isacharbrackright}\ {\isacharequal}\ new\ monoid{\isacharbrackleft}BigInt{\isacharbrackright}\ {\isacharbraceleft}\isanewline
-\ \ val\ {\isacharbackquote}Example{\isachardot}neutral{\isacharbackquote}\ {\isacharequal}\ neutral{\isacharunderscore}int\isanewline
-\ \ val\ {\isacharbackquote}Example{\isachardot}mult{\isacharbackquote}\ {\isacharequal}\ {\isacharparenleft}a{\isacharcolon}\ BigInt{\isacharcomma}\ b{\isacharcolon}\ BigInt{\isacharparenright}\ {\isacharequal}{\isachargreater}\ mult{\isacharunderscore}int{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\isanewline
-{\isacharbraceright}\isanewline
+implicit\ def\ monoid{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{3A}{\isacharcolon}}\ monoid{\isaliteral{5B}{\isacharbrackleft}}BigInt{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ new\ monoid{\isaliteral{5B}{\isacharbrackleft}}BigInt{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
+\ \ val\ {\isaliteral{60}{\isacharbackquote}}Example{\isaliteral{2E}{\isachardot}}neutral{\isaliteral{60}{\isacharbackquote}}\ {\isaliteral{3D}{\isacharequal}}\ neutral{\isaliteral{5F}{\isacharunderscore}}int\isanewline
+\ \ val\ {\isaliteral{60}{\isacharbackquote}}Example{\isaliteral{2E}{\isachardot}}mult{\isaliteral{60}{\isacharbackquote}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ mult{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{29}{\isacharparenright}}\isanewline
+{\isaliteral{7D}{\isacharbraceright}}\isanewline
\isanewline
-def\ inverse{\isacharunderscore}int{\isacharparenleft}i{\isacharcolon}\ BigInt{\isacharparenright}{\isacharcolon}\ BigInt\ {\isacharequal}\ {\isacharparenleft}{\isacharminus}\ i{\isacharparenright}\isanewline
+def\ inverse{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{28}{\isacharparenleft}}i{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{29}{\isacharparenright}}{\isaliteral{3A}{\isacharcolon}}\ BigInt\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2D}{\isacharminus}}\ i{\isaliteral{29}{\isacharparenright}}\isanewline
\isanewline
-implicit\ def\ group{\isacharunderscore}int{\isacharcolon}\ group{\isacharbrackleft}BigInt{\isacharbrackright}\ {\isacharequal}\ new\ group{\isacharbrackleft}BigInt{\isacharbrackright}\ {\isacharbraceleft}\isanewline
-\ \ val\ {\isacharbackquote}Example{\isachardot}inverse{\isacharbackquote}\ {\isacharequal}\ {\isacharparenleft}a{\isacharcolon}\ BigInt{\isacharparenright}\ {\isacharequal}{\isachargreater}\ inverse{\isacharunderscore}int{\isacharparenleft}a{\isacharparenright}\isanewline
-\ \ val\ {\isacharbackquote}Example{\isachardot}neutral{\isacharbackquote}\ {\isacharequal}\ neutral{\isacharunderscore}int\isanewline
-\ \ val\ {\isacharbackquote}Example{\isachardot}mult{\isacharbackquote}\ {\isacharequal}\ {\isacharparenleft}a{\isacharcolon}\ BigInt{\isacharcomma}\ b{\isacharcolon}\ BigInt{\isacharparenright}\ {\isacharequal}{\isachargreater}\ mult{\isacharunderscore}int{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\isanewline
-{\isacharbraceright}\isanewline
+implicit\ def\ group{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{3A}{\isacharcolon}}\ group{\isaliteral{5B}{\isacharbrackleft}}BigInt{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ new\ group{\isaliteral{5B}{\isacharbrackleft}}BigInt{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
+\ \ val\ {\isaliteral{60}{\isacharbackquote}}Example{\isaliteral{2E}{\isachardot}}inverse{\isaliteral{60}{\isacharbackquote}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ inverse{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{29}{\isacharparenright}}\isanewline
+\ \ val\ {\isaliteral{60}{\isacharbackquote}}Example{\isaliteral{2E}{\isachardot}}neutral{\isaliteral{60}{\isacharbackquote}}\ {\isaliteral{3D}{\isacharequal}}\ neutral{\isaliteral{5F}{\isacharunderscore}}int\isanewline
+\ \ val\ {\isaliteral{60}{\isacharbackquote}}Example{\isaliteral{2E}{\isachardot}}mult{\isaliteral{60}{\isacharbackquote}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ mult{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{29}{\isacharparenright}}\isanewline
+{\isaliteral{7D}{\isacharbraceright}}\isanewline
\isanewline
-def\ example{\isacharcolon}\ BigInt\ {\isacharequal}\ pow{\isacharunderscore}int{\isacharbrackleft}BigInt{\isacharbrackright}{\isacharparenleft}BigInt{\isacharparenleft}{\isadigit{1}}{\isadigit{0}}{\isacharparenright}{\isacharcomma}\ BigInt{\isacharparenleft}{\isacharminus}\ {\isadigit{2}}{\isacharparenright}{\isacharparenright}\isanewline
+def\ example{\isaliteral{3A}{\isacharcolon}}\ BigInt\ {\isaliteral{3D}{\isacharequal}}\ pow{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{5B}{\isacharbrackleft}}BigInt{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{28}{\isacharparenleft}}BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ BigInt{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2D}{\isacharminus}}\ {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline
\isanewline
-{\isacharbraceright}\ {\isacharslash}{\isacharasterisk}\ object\ Example\ {\isacharasterisk}{\isacharslash}\isanewline%
+{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{2F}{\isacharslash}}{\isaliteral{2A}{\isacharasterisk}}\ object\ Example\ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{2F}{\isacharslash}}\isanewline%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -1415,10 +1415,10 @@
\begin{description}
- \item[\hyperlink{command.print-classes}{\mbox{\isa{\isacommand{print{\isacharunderscore}classes}}}}] print a list of all classes
+ \item[\hyperlink{command.print-classes}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}classes}}}}] print a list of all classes
together with associated operations etc.
- \item[\hyperlink{command.class-deps}{\mbox{\isa{\isacommand{class{\isacharunderscore}deps}}}}] visualizes the subclass relation
+ \item[\hyperlink{command.class-deps}{\mbox{\isa{\isacommand{class{\isaliteral{5F}{\isacharunderscore}}deps}}}}] visualizes the subclass relation
between all classes as a Hasse diagram.
\end{description}%