26 Type classes were introduced by Wadler and Blott \cite{wadler89how} |
26 Type classes were introduced by Wadler and Blott \cite{wadler89how} |
27 into the Haskell language to allow for a reasonable implementation |
27 into the Haskell language to allow for a reasonable implementation |
28 of overloading\footnote{throughout this tutorial, we are referring |
28 of overloading\footnote{throughout this tutorial, we are referring |
29 to classical Haskell 1.0 type classes, not considering later |
29 to classical Haskell 1.0 type classes, not considering later |
30 additions in expressiveness}. As a canonical example, a polymorphic |
30 additions in expressiveness}. As a canonical example, a polymorphic |
31 equality function \isa{eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} which is overloaded on |
31 equality function \isa{eq\ {\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool} which is overloaded on |
32 different types for \isa{{\isasymalpha}}, which is achieved by splitting |
32 different types for \isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}}, which is achieved by splitting |
33 introduction of the \isa{eq} function from its overloaded |
33 introduction of the \isa{eq} function from its overloaded |
34 definitions by means of \isa{class} and \isa{instance} |
34 definitions by means of \isa{class} and \isa{instance} |
35 declarations: \footnote{syntax here is a kind of isabellized |
35 declarations: \footnote{syntax here is a kind of isabellized |
36 Haskell} |
36 Haskell} |
37 |
37 |
38 \begin{quote} |
38 \begin{quote} |
39 |
39 |
40 \noindent\isa{class\ eq\ where} \\ |
40 \noindent\isa{class\ eq\ where} \\ |
41 \hspace*{2ex}\isa{eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} |
41 \hspace*{2ex}\isa{eq\ {\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool} |
42 |
42 |
43 \medskip\noindent\isa{instance\ nat\ {\isasymColon}\ eq\ where} \\ |
43 \medskip\noindent\isa{instance\ nat\ {\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}\ eq\ where} \\ |
44 \hspace*{2ex}\isa{eq\ {\isadigit{0}}\ {\isadigit{0}}\ {\isacharequal}\ True} \\ |
44 \hspace*{2ex}\isa{eq\ {\isadigit{0}}\ {\isadigit{0}}\ {\isaliteral{3D}{\isacharequal}}\ True} \\ |
45 \hspace*{2ex}\isa{eq\ {\isadigit{0}}\ {\isacharunderscore}\ {\isacharequal}\ False} \\ |
45 \hspace*{2ex}\isa{eq\ {\isadigit{0}}\ {\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{3D}{\isacharequal}}\ False} \\ |
46 \hspace*{2ex}\isa{eq\ {\isacharunderscore}\ {\isadigit{0}}\ {\isacharequal}\ False} \\ |
46 \hspace*{2ex}\isa{eq\ {\isaliteral{5F}{\isacharunderscore}}\ {\isadigit{0}}\ {\isaliteral{3D}{\isacharequal}}\ False} \\ |
47 \hspace*{2ex}\isa{eq\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharparenleft}Suc\ m{\isacharparenright}\ {\isacharequal}\ eq\ n\ m} |
47 \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} |
48 |
48 |
49 \medskip\noindent\isa{instance\ {\isacharparenleft}{\isasymalpha}{\isasymColon}eq{\isacharcomma}\ {\isasymbeta}{\isasymColon}eq{\isacharparenright}\ pair\ {\isasymColon}\ eq\ where} \\ |
49 \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} \\ |
50 \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}}} |
50 \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}}} |
51 |
51 |
52 \medskip\noindent\isa{class\ ord\ extends\ eq\ where} \\ |
52 \medskip\noindent\isa{class\ ord\ extends\ eq\ where} \\ |
53 \hspace*{2ex}\isa{less{\isacharunderscore}eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} \\ |
53 \hspace*{2ex}\isa{less{\isaliteral{5F}{\isacharunderscore}}eq\ {\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool} \\ |
54 \hspace*{2ex}\isa{less\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} |
54 \hspace*{2ex}\isa{less\ {\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool} |
55 |
55 |
56 \end{quote} |
56 \end{quote} |
57 |
57 |
58 \noindent Type variables are annotated with (finitely many) classes; |
58 \noindent Type variables are annotated with (finitely many) classes; |
59 these annotations are assertions that a particular polymorphic type |
59 these annotations are assertions that a particular polymorphic type |
142 % |
142 % |
143 \begin{isamarkuptext}% |
143 \begin{isamarkuptext}% |
144 \noindent This \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}} specification consists of two parts: |
144 \noindent This \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}} specification consists of two parts: |
145 the \qn{operational} part names the class parameter (\hyperlink{element.fixes}{\mbox{\isa{\isakeyword{fixes}}}}), the \qn{logical} part specifies properties on them |
145 the \qn{operational} part names the class parameter (\hyperlink{element.fixes}{\mbox{\isa{\isakeyword{fixes}}}}), the \qn{logical} part specifies properties on them |
146 (\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 |
146 (\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 |
147 parameter \isa{{\isachardoublequote}mult\ {\isasymColon}\ {\isasymalpha}{\isasymColon}semigroup\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequote}} and the |
147 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 |
148 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}}.% |
148 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}}}.% |
149 \end{isamarkuptext}% |
149 \end{isamarkuptext}% |
150 \isamarkuptrue% |
150 \isamarkuptrue% |
151 % |
151 % |
152 \isamarkupsubsection{Class instantiation \label{sec:class_inst}% |
152 \isamarkupsubsection{Class instantiation \label{sec:class_inst}% |
153 } |
153 } |
154 \isamarkuptrue% |
154 \isamarkuptrue% |
155 % |
155 % |
156 \begin{isamarkuptext}% |
156 \begin{isamarkuptext}% |
157 The concrete type \isa{int} is made a \isa{semigroup} instance |
157 The concrete type \isa{int} is made a \isa{semigroup} instance |
158 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 |
158 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 |
159 accomplished by the \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}} target:% |
159 accomplished by the \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}} target:% |
160 \end{isamarkuptext}% |
160 \end{isamarkuptext}% |
161 \isamarkuptrue% |
161 \isamarkuptrue% |
162 % |
162 % |
163 \isadelimquote |
163 \isadelimquote |
164 % |
164 % |
165 \endisadelimquote |
165 \endisadelimquote |
166 % |
166 % |
167 \isatagquote |
167 \isatagquote |
168 \isacommand{instantiation}\isamarkupfalse% |
168 \isacommand{instantiation}\isamarkupfalse% |
169 \ int\ {\isacharcolon}{\isacharcolon}\ semigroup\isanewline |
169 \ int\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ semigroup\isanewline |
170 \isakeyword{begin}\isanewline |
170 \isakeyword{begin}\isanewline |
171 \isanewline |
171 \isanewline |
172 \isacommand{definition}\isamarkupfalse% |
172 \isacommand{definition}\isamarkupfalse% |
173 \isanewline |
173 \isanewline |
174 \ \ mult{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}i\ {\isasymotimes}\ j\ {\isacharequal}\ i\ {\isacharplus}\ {\isacharparenleft}j{\isasymColon}int{\isacharparenright}{\isachardoublequoteclose}\isanewline |
174 \ \ 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 |
175 \isanewline |
175 \isanewline |
176 \isacommand{instance}\isamarkupfalse% |
176 \isacommand{instance}\isamarkupfalse% |
177 \ \isacommand{proof}\isamarkupfalse% |
177 \ \isacommand{proof}\isamarkupfalse% |
178 \isanewline |
178 \isanewline |
179 \ \ \isacommand{fix}\isamarkupfalse% |
179 \ \ \isacommand{fix}\isamarkupfalse% |
180 \ i\ j\ k\ {\isacharcolon}{\isacharcolon}\ int\ \isacommand{have}\isamarkupfalse% |
180 \ i\ j\ k\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ int\ \isacommand{have}\isamarkupfalse% |
181 \ {\isachardoublequoteopen}{\isacharparenleft}i\ {\isacharplus}\ j{\isacharparenright}\ {\isacharplus}\ k\ {\isacharequal}\ i\ {\isacharplus}\ {\isacharparenleft}j\ {\isacharplus}\ k{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% |
181 \ {\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% |
182 \ simp\isanewline |
182 \ simp\isanewline |
183 \ \ \isacommand{then}\isamarkupfalse% |
183 \ \ \isacommand{then}\isamarkupfalse% |
184 \ \isacommand{show}\isamarkupfalse% |
184 \ \isacommand{show}\isamarkupfalse% |
185 \ {\isachardoublequoteopen}{\isacharparenleft}i\ {\isasymotimes}\ j{\isacharparenright}\ {\isasymotimes}\ k\ {\isacharequal}\ i\ {\isasymotimes}\ {\isacharparenleft}j\ {\isasymotimes}\ k{\isacharparenright}{\isachardoublequoteclose}\isanewline |
185 \ {\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 |
186 \ \ \ \ \isacommand{unfolding}\isamarkupfalse% |
186 \ \ \ \ \isacommand{unfolding}\isamarkupfalse% |
187 \ mult{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{{\isachardot}}\isamarkupfalse% |
187 \ mult{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{5F}{\isacharunderscore}}def\ \isacommand{{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% |
188 \isanewline |
188 \isanewline |
189 \isacommand{qed}\isamarkupfalse% |
189 \isacommand{qed}\isamarkupfalse% |
190 \isanewline |
190 \isanewline |
191 \isanewline |
191 \isanewline |
192 \isacommand{end}\isamarkupfalse% |
192 \isacommand{end}\isamarkupfalse% |
275 % |
275 % |
276 \endisadelimquote |
276 \endisadelimquote |
277 % |
277 % |
278 \isatagquote |
278 \isatagquote |
279 \isacommand{instantiation}\isamarkupfalse% |
279 \isacommand{instantiation}\isamarkupfalse% |
280 \ prod\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}semigroup{\isacharcomma}\ semigroup{\isacharparenright}\ semigroup\isanewline |
280 \ prod\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}semigroup{\isaliteral{2C}{\isacharcomma}}\ semigroup{\isaliteral{29}{\isacharparenright}}\ semigroup\isanewline |
281 \isakeyword{begin}\isanewline |
281 \isakeyword{begin}\isanewline |
282 \isanewline |
282 \isanewline |
283 \isacommand{definition}\isamarkupfalse% |
283 \isacommand{definition}\isamarkupfalse% |
284 \isanewline |
284 \isanewline |
285 \ \ 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 |
285 \ \ 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 |
286 \isanewline |
286 \isanewline |
287 \isacommand{instance}\isamarkupfalse% |
287 \isacommand{instance}\isamarkupfalse% |
288 \ \isacommand{proof}\isamarkupfalse% |
288 \ \isacommand{proof}\isamarkupfalse% |
289 \isanewline |
289 \isanewline |
290 \ \ \isacommand{fix}\isamarkupfalse% |
290 \ \ \isacommand{fix}\isamarkupfalse% |
291 \ p\isactrlisub {\isadigit{1}}\ p\isactrlisub {\isadigit{2}}\ p\isactrlisub {\isadigit{3}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isasymColon}semigroup\ {\isasymtimes}\ {\isasymbeta}{\isasymColon}semigroup{\isachardoublequoteclose}\isanewline |
291 \ 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 |
292 \ \ \isacommand{show}\isamarkupfalse% |
292 \ \ \isacommand{show}\isamarkupfalse% |
293 \ {\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 |
293 \ {\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 |
294 \ \ \ \ \isacommand{unfolding}\isamarkupfalse% |
294 \ \ \ \ \isacommand{unfolding}\isamarkupfalse% |
295 \ mult{\isacharunderscore}prod{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% |
295 \ mult{\isaliteral{5F}{\isacharunderscore}}prod{\isaliteral{5F}{\isacharunderscore}}def\ \isacommand{by}\isamarkupfalse% |
296 \ {\isacharparenleft}simp\ add{\isacharcolon}\ assoc{\isacharparenright}\isanewline |
296 \ {\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ assoc{\isaliteral{29}{\isacharparenright}}\isanewline |
297 \isacommand{qed}\isamarkupfalse% |
297 \isacommand{qed}\isamarkupfalse% |
298 \ \ \ \ \ \ \isanewline |
298 \ \ \ \ \ \ \isanewline |
299 \isanewline |
299 \isanewline |
300 \isacommand{end}\isamarkupfalse% |
300 \isacommand{end}\isamarkupfalse% |
301 % |
301 % |
355 % |
355 % |
356 \endisadelimquote |
356 \endisadelimquote |
357 % |
357 % |
358 \isatagquote |
358 \isatagquote |
359 \isacommand{instantiation}\isamarkupfalse% |
359 \isacommand{instantiation}\isamarkupfalse% |
360 \ nat\ \isakeyword{and}\ int\ {\isacharcolon}{\isacharcolon}\ monoidl\isanewline |
360 \ nat\ \isakeyword{and}\ int\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ monoidl\isanewline |
361 \isakeyword{begin}\isanewline |
361 \isakeyword{begin}\isanewline |
362 \isanewline |
362 \isanewline |
363 \isacommand{definition}\isamarkupfalse% |
363 \isacommand{definition}\isamarkupfalse% |
364 \isanewline |
364 \isanewline |
365 \ \ neutral{\isacharunderscore}nat{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}nat{\isacharparenright}{\isachardoublequoteclose}\isanewline |
365 \ \ 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 |
366 \isanewline |
366 \isanewline |
367 \isacommand{definition}\isamarkupfalse% |
367 \isacommand{definition}\isamarkupfalse% |
368 \isanewline |
368 \isanewline |
369 \ \ neutral{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}int{\isacharparenright}{\isachardoublequoteclose}\isanewline |
369 \ \ 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 |
370 \isanewline |
370 \isanewline |
371 \isacommand{instance}\isamarkupfalse% |
371 \isacommand{instance}\isamarkupfalse% |
372 \ \isacommand{proof}\isamarkupfalse% |
372 \ \isacommand{proof}\isamarkupfalse% |
373 \isanewline |
373 \isanewline |
374 \ \ \isacommand{fix}\isamarkupfalse% |
374 \ \ \isacommand{fix}\isamarkupfalse% |
375 \ n\ {\isacharcolon}{\isacharcolon}\ nat\isanewline |
375 \ n\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ nat\isanewline |
376 \ \ \isacommand{show}\isamarkupfalse% |
376 \ \ \isacommand{show}\isamarkupfalse% |
377 \ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline |
377 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6F6E653E}{\isasymone}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ n\ {\isaliteral{3D}{\isacharequal}}\ n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
378 \ \ \ \ \isacommand{unfolding}\isamarkupfalse% |
378 \ \ \ \ \isacommand{unfolding}\isamarkupfalse% |
379 \ neutral{\isacharunderscore}nat{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% |
379 \ neutral{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{5F}{\isacharunderscore}}def\ \isacommand{by}\isamarkupfalse% |
380 \ simp\isanewline |
380 \ simp\isanewline |
381 \isacommand{next}\isamarkupfalse% |
381 \isacommand{next}\isamarkupfalse% |
382 \isanewline |
382 \isanewline |
383 \ \ \isacommand{fix}\isamarkupfalse% |
383 \ \ \isacommand{fix}\isamarkupfalse% |
384 \ k\ {\isacharcolon}{\isacharcolon}\ int\isanewline |
384 \ k\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ int\isanewline |
385 \ \ \isacommand{show}\isamarkupfalse% |
385 \ \ \isacommand{show}\isamarkupfalse% |
386 \ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ k\ {\isacharequal}\ k{\isachardoublequoteclose}\isanewline |
386 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6F6E653E}{\isasymone}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ k\ {\isaliteral{3D}{\isacharequal}}\ k{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
387 \ \ \ \ \isacommand{unfolding}\isamarkupfalse% |
387 \ \ \ \ \isacommand{unfolding}\isamarkupfalse% |
388 \ neutral{\isacharunderscore}int{\isacharunderscore}def\ mult{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% |
388 \ neutral{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{5F}{\isacharunderscore}}def\ mult{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{5F}{\isacharunderscore}}def\ \isacommand{by}\isamarkupfalse% |
389 \ simp\isanewline |
389 \ simp\isanewline |
390 \isacommand{qed}\isamarkupfalse% |
390 \isacommand{qed}\isamarkupfalse% |
391 \isanewline |
391 \isanewline |
392 \isanewline |
392 \isanewline |
393 \isacommand{end}\isamarkupfalse% |
393 \isacommand{end}\isamarkupfalse% |
394 \isanewline |
394 \isanewline |
395 \isanewline |
395 \isanewline |
396 \isacommand{instantiation}\isamarkupfalse% |
396 \isacommand{instantiation}\isamarkupfalse% |
397 \ prod\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}monoidl{\isacharcomma}\ monoidl{\isacharparenright}\ monoidl\isanewline |
397 \ prod\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}monoidl{\isaliteral{2C}{\isacharcomma}}\ monoidl{\isaliteral{29}{\isacharparenright}}\ monoidl\isanewline |
398 \isakeyword{begin}\isanewline |
398 \isakeyword{begin}\isanewline |
399 \isanewline |
399 \isanewline |
400 \isacommand{definition}\isamarkupfalse% |
400 \isacommand{definition}\isamarkupfalse% |
401 \isanewline |
401 \isanewline |
402 \ \ neutral{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isacharequal}\ {\isacharparenleft}{\isasymone}{\isacharcomma}\ {\isasymone}{\isacharparenright}{\isachardoublequoteclose}\isanewline |
402 \ \ 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 |
403 \isanewline |
403 \isanewline |
404 \isacommand{instance}\isamarkupfalse% |
404 \isacommand{instance}\isamarkupfalse% |
405 \ \isacommand{proof}\isamarkupfalse% |
405 \ \isacommand{proof}\isamarkupfalse% |
406 \isanewline |
406 \isanewline |
407 \ \ \isacommand{fix}\isamarkupfalse% |
407 \ \ \isacommand{fix}\isamarkupfalse% |
408 \ p\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isasymColon}monoidl\ {\isasymtimes}\ {\isasymbeta}{\isasymColon}monoidl{\isachardoublequoteclose}\isanewline |
408 \ 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 |
409 \ \ \isacommand{show}\isamarkupfalse% |
409 \ \ \isacommand{show}\isamarkupfalse% |
410 \ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ p\ {\isacharequal}\ p{\isachardoublequoteclose}\isanewline |
410 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6F6E653E}{\isasymone}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ p\ {\isaliteral{3D}{\isacharequal}}\ p{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
411 \ \ \ \ \isacommand{unfolding}\isamarkupfalse% |
411 \ \ \ \ \isacommand{unfolding}\isamarkupfalse% |
412 \ neutral{\isacharunderscore}prod{\isacharunderscore}def\ mult{\isacharunderscore}prod{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% |
412 \ neutral{\isaliteral{5F}{\isacharunderscore}}prod{\isaliteral{5F}{\isacharunderscore}}def\ mult{\isaliteral{5F}{\isacharunderscore}}prod{\isaliteral{5F}{\isacharunderscore}}def\ \isacommand{by}\isamarkupfalse% |
413 \ {\isacharparenleft}simp\ add{\isacharcolon}\ neutl{\isacharparenright}\isanewline |
413 \ {\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ neutl{\isaliteral{29}{\isacharparenright}}\isanewline |
414 \isacommand{qed}\isamarkupfalse% |
414 \isacommand{qed}\isamarkupfalse% |
415 \isanewline |
415 \isanewline |
416 \isanewline |
416 \isanewline |
417 \isacommand{end}\isamarkupfalse% |
417 \isacommand{end}\isamarkupfalse% |
418 % |
418 % |
433 % |
433 % |
434 \endisadelimquote |
434 \endisadelimquote |
435 % |
435 % |
436 \isatagquote |
436 \isatagquote |
437 \isacommand{class}\isamarkupfalse% |
437 \isacommand{class}\isamarkupfalse% |
438 \ monoid\ {\isacharequal}\ monoidl\ {\isacharplus}\isanewline |
438 \ monoid\ {\isaliteral{3D}{\isacharequal}}\ monoidl\ {\isaliteral{2B}{\isacharplus}}\isanewline |
439 \ \ \isakeyword{assumes}\ neutr{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline |
439 \ \ \isakeyword{assumes}\ neutr{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ {\isaliteral{5C3C6F6E653E}{\isasymone}}\ {\isaliteral{3D}{\isacharequal}}\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
440 \isanewline |
440 \isanewline |
441 \isacommand{instantiation}\isamarkupfalse% |
441 \isacommand{instantiation}\isamarkupfalse% |
442 \ nat\ \isakeyword{and}\ int\ {\isacharcolon}{\isacharcolon}\ monoid\ \isanewline |
442 \ nat\ \isakeyword{and}\ int\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ monoid\ \isanewline |
443 \isakeyword{begin}\isanewline |
443 \isakeyword{begin}\isanewline |
444 \isanewline |
444 \isanewline |
445 \isacommand{instance}\isamarkupfalse% |
445 \isacommand{instance}\isamarkupfalse% |
446 \ \isacommand{proof}\isamarkupfalse% |
446 \ \isacommand{proof}\isamarkupfalse% |
447 \isanewline |
447 \isanewline |
448 \ \ \isacommand{fix}\isamarkupfalse% |
448 \ \ \isacommand{fix}\isamarkupfalse% |
449 \ n\ {\isacharcolon}{\isacharcolon}\ nat\isanewline |
449 \ n\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ nat\isanewline |
450 \ \ \isacommand{show}\isamarkupfalse% |
450 \ \ \isacommand{show}\isamarkupfalse% |
451 \ {\isachardoublequoteopen}n\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline |
451 \ {\isaliteral{22}{\isachardoublequoteopen}}n\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ {\isaliteral{5C3C6F6E653E}{\isasymone}}\ {\isaliteral{3D}{\isacharequal}}\ n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
452 \ \ \ \ \isacommand{unfolding}\isamarkupfalse% |
452 \ \ \ \ \isacommand{unfolding}\isamarkupfalse% |
453 \ neutral{\isacharunderscore}nat{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% |
453 \ neutral{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{5F}{\isacharunderscore}}def\ \isacommand{by}\isamarkupfalse% |
454 \ {\isacharparenleft}induct\ n{\isacharparenright}\ simp{\isacharunderscore}all\isanewline |
454 \ {\isaliteral{28}{\isacharparenleft}}induct\ n{\isaliteral{29}{\isacharparenright}}\ simp{\isaliteral{5F}{\isacharunderscore}}all\isanewline |
455 \isacommand{next}\isamarkupfalse% |
455 \isacommand{next}\isamarkupfalse% |
456 \isanewline |
456 \isanewline |
457 \ \ \isacommand{fix}\isamarkupfalse% |
457 \ \ \isacommand{fix}\isamarkupfalse% |
458 \ k\ {\isacharcolon}{\isacharcolon}\ int\isanewline |
458 \ k\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ int\isanewline |
459 \ \ \isacommand{show}\isamarkupfalse% |
459 \ \ \isacommand{show}\isamarkupfalse% |
460 \ {\isachardoublequoteopen}k\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ k{\isachardoublequoteclose}\isanewline |
460 \ {\isaliteral{22}{\isachardoublequoteopen}}k\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ {\isaliteral{5C3C6F6E653E}{\isasymone}}\ {\isaliteral{3D}{\isacharequal}}\ k{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
461 \ \ \ \ \isacommand{unfolding}\isamarkupfalse% |
461 \ \ \ \ \isacommand{unfolding}\isamarkupfalse% |
462 \ neutral{\isacharunderscore}int{\isacharunderscore}def\ mult{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% |
462 \ neutral{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{5F}{\isacharunderscore}}def\ mult{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{5F}{\isacharunderscore}}def\ \isacommand{by}\isamarkupfalse% |
463 \ simp\isanewline |
463 \ simp\isanewline |
464 \isacommand{qed}\isamarkupfalse% |
464 \isacommand{qed}\isamarkupfalse% |
465 \isanewline |
465 \isanewline |
466 \isanewline |
466 \isanewline |
467 \isacommand{end}\isamarkupfalse% |
467 \isacommand{end}\isamarkupfalse% |
468 \isanewline |
468 \isanewline |
469 \isanewline |
469 \isanewline |
470 \isacommand{instantiation}\isamarkupfalse% |
470 \isacommand{instantiation}\isamarkupfalse% |
471 \ prod\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}monoid{\isacharcomma}\ monoid{\isacharparenright}\ monoid\isanewline |
471 \ prod\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}monoid{\isaliteral{2C}{\isacharcomma}}\ monoid{\isaliteral{29}{\isacharparenright}}\ monoid\isanewline |
472 \isakeyword{begin}\isanewline |
472 \isakeyword{begin}\isanewline |
473 \isanewline |
473 \isanewline |
474 \isacommand{instance}\isamarkupfalse% |
474 \isacommand{instance}\isamarkupfalse% |
475 \ \isacommand{proof}\isamarkupfalse% |
475 \ \isacommand{proof}\isamarkupfalse% |
476 \ \isanewline |
476 \ \isanewline |
477 \ \ \isacommand{fix}\isamarkupfalse% |
477 \ \ \isacommand{fix}\isamarkupfalse% |
478 \ p\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isasymColon}monoid\ {\isasymtimes}\ {\isasymbeta}{\isasymColon}monoid{\isachardoublequoteclose}\isanewline |
478 \ 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 |
479 \ \ \isacommand{show}\isamarkupfalse% |
479 \ \ \isacommand{show}\isamarkupfalse% |
480 \ {\isachardoublequoteopen}p\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ p{\isachardoublequoteclose}\isanewline |
480 \ {\isaliteral{22}{\isachardoublequoteopen}}p\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ {\isaliteral{5C3C6F6E653E}{\isasymone}}\ {\isaliteral{3D}{\isacharequal}}\ p{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
481 \ \ \ \ \isacommand{unfolding}\isamarkupfalse% |
481 \ \ \ \ \isacommand{unfolding}\isamarkupfalse% |
482 \ neutral{\isacharunderscore}prod{\isacharunderscore}def\ mult{\isacharunderscore}prod{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% |
482 \ neutral{\isaliteral{5F}{\isacharunderscore}}prod{\isaliteral{5F}{\isacharunderscore}}def\ mult{\isaliteral{5F}{\isacharunderscore}}prod{\isaliteral{5F}{\isacharunderscore}}def\ \isacommand{by}\isamarkupfalse% |
483 \ {\isacharparenleft}simp\ add{\isacharcolon}\ neutr{\isacharparenright}\isanewline |
483 \ {\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ neutr{\isaliteral{29}{\isacharparenright}}\isanewline |
484 \isacommand{qed}\isamarkupfalse% |
484 \isacommand{qed}\isamarkupfalse% |
485 \isanewline |
485 \isanewline |
486 \isanewline |
486 \isanewline |
487 \isacommand{end}\isamarkupfalse% |
487 \isacommand{end}\isamarkupfalse% |
488 % |
488 % |
502 % |
502 % |
503 \endisadelimquote |
503 \endisadelimquote |
504 % |
504 % |
505 \isatagquote |
505 \isatagquote |
506 \isacommand{class}\isamarkupfalse% |
506 \isacommand{class}\isamarkupfalse% |
507 \ group\ {\isacharequal}\ monoidl\ {\isacharplus}\isanewline |
507 \ group\ {\isaliteral{3D}{\isacharequal}}\ monoidl\ {\isaliteral{2B}{\isacharplus}}\isanewline |
508 \ \ \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 |
508 \ \ \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 |
509 \ \ \isakeyword{assumes}\ invl{\isacharcolon}\ {\isachardoublequoteopen}x{\isasymdiv}\ {\isasymotimes}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline |
509 \ \ \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 |
510 \isanewline |
510 \isanewline |
511 \isacommand{instantiation}\isamarkupfalse% |
511 \isacommand{instantiation}\isamarkupfalse% |
512 \ int\ {\isacharcolon}{\isacharcolon}\ group\isanewline |
512 \ int\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ group\isanewline |
513 \isakeyword{begin}\isanewline |
513 \isakeyword{begin}\isanewline |
514 \isanewline |
514 \isanewline |
515 \isacommand{definition}\isamarkupfalse% |
515 \isacommand{definition}\isamarkupfalse% |
516 \isanewline |
516 \isanewline |
517 \ \ inverse{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}i{\isasymdiv}\ {\isacharequal}\ {\isacharminus}\ {\isacharparenleft}i{\isasymColon}int{\isacharparenright}{\isachardoublequoteclose}\isanewline |
517 \ \ 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 |
518 \isanewline |
518 \isanewline |
519 \isacommand{instance}\isamarkupfalse% |
519 \isacommand{instance}\isamarkupfalse% |
520 \ \isacommand{proof}\isamarkupfalse% |
520 \ \isacommand{proof}\isamarkupfalse% |
521 \isanewline |
521 \isanewline |
522 \ \ \isacommand{fix}\isamarkupfalse% |
522 \ \ \isacommand{fix}\isamarkupfalse% |
523 \ i\ {\isacharcolon}{\isacharcolon}\ int\isanewline |
523 \ i\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ int\isanewline |
524 \ \ \isacommand{have}\isamarkupfalse% |
524 \ \ \isacommand{have}\isamarkupfalse% |
525 \ {\isachardoublequoteopen}{\isacharminus}i\ {\isacharplus}\ i\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% |
525 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{2D}{\isacharminus}}i\ {\isaliteral{2B}{\isacharplus}}\ i\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse% |
526 \ simp\isanewline |
526 \ simp\isanewline |
527 \ \ \isacommand{then}\isamarkupfalse% |
527 \ \ \isacommand{then}\isamarkupfalse% |
528 \ \isacommand{show}\isamarkupfalse% |
528 \ \isacommand{show}\isamarkupfalse% |
529 \ {\isachardoublequoteopen}i{\isasymdiv}\ {\isasymotimes}\ i\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline |
529 \ {\isaliteral{22}{\isachardoublequoteopen}}i{\isaliteral{5C3C6469763E}{\isasymdiv}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ i\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C6F6E653E}{\isasymone}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
530 \ \ \ \ \isacommand{unfolding}\isamarkupfalse% |
530 \ \ \ \ \isacommand{unfolding}\isamarkupfalse% |
531 \ mult{\isacharunderscore}int{\isacharunderscore}def\ neutral{\isacharunderscore}int{\isacharunderscore}def\ inverse{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{{\isachardot}}\isamarkupfalse% |
531 \ 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% |
532 \isanewline |
532 \isanewline |
533 \isacommand{qed}\isamarkupfalse% |
533 \isacommand{qed}\isamarkupfalse% |
534 \isanewline |
534 \isanewline |
535 \isanewline |
535 \isanewline |
536 \isacommand{end}\isamarkupfalse% |
536 \isacommand{end}\isamarkupfalse% |
718 \isamarkuptrue% |
718 \isamarkuptrue% |
719 % |
719 % |
720 \begin{isamarkuptext}% |
720 \begin{isamarkuptext}% |
721 Isabelle locales enable reasoning at a general level, while results |
721 Isabelle locales enable reasoning at a general level, while results |
722 are implicitly transferred to all instances. For example, we can |
722 are implicitly transferred to all instances. For example, we can |
723 now establish the \isa{left{\isacharunderscore}cancel} lemma for groups, which |
723 now establish the \isa{left{\isaliteral{5F}{\isacharunderscore}}cancel} lemma for groups, which |
724 states that the function \isa{{\isacharparenleft}x\ {\isasymotimes}{\isacharparenright}} is injective:% |
724 states that the function \isa{{\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}{\isaliteral{29}{\isacharparenright}}} is injective:% |
725 \end{isamarkuptext}% |
725 \end{isamarkuptext}% |
726 \isamarkuptrue% |
726 \isamarkuptrue% |
727 % |
727 % |
728 \isadelimquote |
728 \isadelimquote |
729 % |
729 % |
730 \endisadelimquote |
730 \endisadelimquote |
731 % |
731 % |
732 \isatagquote |
732 \isatagquote |
733 \isacommand{lemma}\isamarkupfalse% |
733 \isacommand{lemma}\isamarkupfalse% |
734 \ {\isacharparenleft}\isakeyword{in}\ group{\isacharparenright}\ left{\isacharunderscore}cancel{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequoteclose}\isanewline |
734 \ {\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 |
735 \isacommand{proof}\isamarkupfalse% |
735 \isacommand{proof}\isamarkupfalse% |
736 \isanewline |
736 \isanewline |
737 \ \ \isacommand{assume}\isamarkupfalse% |
737 \ \ \isacommand{assume}\isamarkupfalse% |
738 \ {\isachardoublequoteopen}x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z{\isachardoublequoteclose}\isanewline |
738 \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ y\ {\isaliteral{3D}{\isacharequal}}\ x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ z{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
739 \ \ \isacommand{then}\isamarkupfalse% |
739 \ \ \isacommand{then}\isamarkupfalse% |
740 \ \isacommand{have}\isamarkupfalse% |
740 \ \isacommand{have}\isamarkupfalse% |
741 \ {\isachardoublequoteopen}x{\isasymdiv}\ {\isasymotimes}\ {\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isacharequal}\ x{\isasymdiv}\ {\isasymotimes}\ {\isacharparenleft}x\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% |
741 \ {\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% |
742 \ simp\isanewline |
742 \ simp\isanewline |
743 \ \ \isacommand{then}\isamarkupfalse% |
743 \ \ \isacommand{then}\isamarkupfalse% |
744 \ \isacommand{have}\isamarkupfalse% |
744 \ \isacommand{have}\isamarkupfalse% |
745 \ {\isachardoublequoteopen}{\isacharparenleft}x{\isasymdiv}\ {\isasymotimes}\ x{\isacharparenright}\ {\isasymotimes}\ y\ {\isacharequal}\ {\isacharparenleft}x{\isasymdiv}\ {\isasymotimes}\ x{\isacharparenright}\ {\isasymotimes}\ z{\isachardoublequoteclose}\ \isacommand{using}\isamarkupfalse% |
745 \ {\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% |
746 \ assoc\ \isacommand{by}\isamarkupfalse% |
746 \ assoc\ \isacommand{by}\isamarkupfalse% |
747 \ simp\isanewline |
747 \ simp\isanewline |
748 \ \ \isacommand{then}\isamarkupfalse% |
748 \ \ \isacommand{then}\isamarkupfalse% |
749 \ \isacommand{show}\isamarkupfalse% |
749 \ \isacommand{show}\isamarkupfalse% |
750 \ {\isachardoublequoteopen}y\ {\isacharequal}\ z{\isachardoublequoteclose}\ \isacommand{using}\isamarkupfalse% |
750 \ {\isaliteral{22}{\isachardoublequoteopen}}y\ {\isaliteral{3D}{\isacharequal}}\ z{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{using}\isamarkupfalse% |
751 \ neutl\ \isakeyword{and}\ invl\ \isacommand{by}\isamarkupfalse% |
751 \ neutl\ \isakeyword{and}\ invl\ \isacommand{by}\isamarkupfalse% |
752 \ simp\isanewline |
752 \ simp\isanewline |
753 \isacommand{next}\isamarkupfalse% |
753 \isacommand{next}\isamarkupfalse% |
754 \isanewline |
754 \isanewline |
755 \ \ \isacommand{assume}\isamarkupfalse% |
755 \ \ \isacommand{assume}\isamarkupfalse% |
756 \ {\isachardoublequoteopen}y\ {\isacharequal}\ z{\isachardoublequoteclose}\isanewline |
756 \ {\isaliteral{22}{\isachardoublequoteopen}}y\ {\isaliteral{3D}{\isacharequal}}\ z{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
757 \ \ \isacommand{then}\isamarkupfalse% |
757 \ \ \isacommand{then}\isamarkupfalse% |
758 \ \isacommand{show}\isamarkupfalse% |
758 \ \isacommand{show}\isamarkupfalse% |
759 \ {\isachardoublequoteopen}x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% |
759 \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ y\ {\isaliteral{3D}{\isacharequal}}\ x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ z{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse% |
760 \ simp\isanewline |
760 \ simp\isanewline |
761 \isacommand{qed}\isamarkupfalse% |
761 \isacommand{qed}\isamarkupfalse% |
762 % |
762 % |
763 \endisatagquote |
763 \endisatagquote |
764 {\isafoldquote}% |
764 {\isafoldquote}% |
865 % |
865 % |
866 \endisadelimquote |
866 \endisadelimquote |
867 % |
867 % |
868 \isatagquote |
868 \isatagquote |
869 \isacommand{primrec}\isamarkupfalse% |
869 \isacommand{primrec}\isamarkupfalse% |
870 \ replicate\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isasymalpha}\ list\ {\isasymRightarrow}\ {\isasymalpha}\ list{\isachardoublequoteclose}\ \isakeyword{where}\isanewline |
870 \ 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 |
871 \ \ {\isachardoublequoteopen}replicate\ {\isadigit{0}}\ {\isacharunderscore}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline |
871 \ \ {\isaliteral{22}{\isachardoublequoteopen}}replicate\ {\isadigit{0}}\ {\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
872 \ \ {\isacharbar}\ {\isachardoublequoteopen}replicate\ {\isacharparenleft}Suc\ n{\isacharparenright}\ xs\ {\isacharequal}\ xs\ {\isacharat}\ replicate\ n\ xs{\isachardoublequoteclose}\isanewline |
872 \ \ {\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 |
873 \isanewline |
873 \isanewline |
874 \isacommand{interpretation}\isamarkupfalse% |
874 \isacommand{interpretation}\isamarkupfalse% |
875 \ list{\isacharunderscore}monoid{\isacharcolon}\ monoid\ append\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\ \isakeyword{where}\isanewline |
875 \ 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 |
876 \ \ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ append\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ replicate{\isachardoublequoteclose}\isanewline |
876 \ \ {\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 |
877 \isacommand{proof}\isamarkupfalse% |
877 \isacommand{proof}\isamarkupfalse% |
878 \ {\isacharminus}\isanewline |
878 \ {\isaliteral{2D}{\isacharminus}}\isanewline |
879 \ \ \isacommand{interpret}\isamarkupfalse% |
879 \ \ \isacommand{interpret}\isamarkupfalse% |
880 \ monoid\ append\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
880 \ monoid\ append\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% |
881 \isanewline |
881 \isanewline |
882 \ \ \isacommand{show}\isamarkupfalse% |
882 \ \ \isacommand{show}\isamarkupfalse% |
883 \ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ append\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ replicate{\isachardoublequoteclose}\isanewline |
883 \ {\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 |
884 \ \ \isacommand{proof}\isamarkupfalse% |
884 \ \ \isacommand{proof}\isamarkupfalse% |
885 \isanewline |
885 \isanewline |
886 \ \ \ \ \isacommand{fix}\isamarkupfalse% |
886 \ \ \ \ \isacommand{fix}\isamarkupfalse% |
887 \ n\isanewline |
887 \ n\isanewline |
888 \ \ \ \ \isacommand{show}\isamarkupfalse% |
888 \ \ \ \ \isacommand{show}\isamarkupfalse% |
889 \ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ append\ {\isacharbrackleft}{\isacharbrackright}\ n\ {\isacharequal}\ replicate\ n{\isachardoublequoteclose}\isanewline |
889 \ {\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 |
890 \ \ \ \ \ \ \isacommand{by}\isamarkupfalse% |
890 \ \ \ \ \ \ \isacommand{by}\isamarkupfalse% |
891 \ {\isacharparenleft}induct\ n{\isacharparenright}\ auto\isanewline |
891 \ {\isaliteral{28}{\isacharparenleft}}induct\ n{\isaliteral{29}{\isacharparenright}}\ auto\isanewline |
892 \ \ \isacommand{qed}\isamarkupfalse% |
892 \ \ \isacommand{qed}\isamarkupfalse% |
893 \isanewline |
893 \isanewline |
894 \isacommand{qed}\isamarkupfalse% |
894 \isacommand{qed}\isamarkupfalse% |
895 \ intro{\isacharunderscore}locales% |
895 \ intro{\isaliteral{5F}{\isacharunderscore}}locales% |
896 \endisatagquote |
896 \endisatagquote |
897 {\isafoldquote}% |
897 {\isafoldquote}% |
898 % |
898 % |
899 \isadelimquote |
899 \isadelimquote |
900 % |
900 % |
983 \put(15,35){\vector(-1,-1){10}} |
983 \put(15,35){\vector(-1,-1){10}} |
984 \put(05,15){\vector(3,-1){30}} |
984 \put(05,15){\vector(3,-1){30}} |
985 \end{picture} |
985 \end{picture} |
986 \caption{Subclass relationship of monoids and groups: |
986 \caption{Subclass relationship of monoids and groups: |
987 before and after establishing the relationship |
987 before and after establishing the relationship |
988 \isa{group\ {\isasymsubseteq}\ monoid}; transitive edges are left out.} |
988 \isa{group\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ monoid}; transitive edges are left out.} |
989 \label{fig:subclass} |
989 \label{fig:subclass} |
990 \end{center} |
990 \end{center} |
991 \end{figure} |
991 \end{figure} |
992 |
992 |
993 For illustration, a derived definition in \isa{group} using \isa{pow{\isacharunderscore}nat}% |
993 For illustration, a derived definition in \isa{group} using \isa{pow{\isaliteral{5F}{\isacharunderscore}}nat}% |
994 \end{isamarkuptext}% |
994 \end{isamarkuptext}% |
995 \isamarkuptrue% |
995 \isamarkuptrue% |
996 % |
996 % |
997 \isadelimquote |
997 \isadelimquote |
998 % |
998 % |
999 \endisadelimquote |
999 \endisadelimquote |
1000 % |
1000 % |
1001 \isatagquote |
1001 \isatagquote |
1002 \isacommand{definition}\isamarkupfalse% |
1002 \isacommand{definition}\isamarkupfalse% |
1003 \ {\isacharparenleft}\isakeyword{in}\ group{\isacharparenright}\ pow{\isacharunderscore}int\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}int\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \isakeyword{where}\isanewline |
1003 \ {\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 |
1004 \ \ {\isachardoublequoteopen}pow{\isacharunderscore}int\ k\ x\ {\isacharequal}\ {\isacharparenleft}if\ k\ {\isachargreater}{\isacharequal}\ {\isadigit{0}}\isanewline |
1004 \ \ {\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 |
1005 \ \ \ \ then\ pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ k{\isacharparenright}\ x\isanewline |
1005 \ \ \ \ then\ pow{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{28}{\isacharparenleft}}nat\ k{\isaliteral{29}{\isacharparenright}}\ x\isanewline |
1006 \ \ \ \ else\ {\isacharparenleft}pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ {\isacharparenleft}{\isacharminus}\ k{\isacharparenright}{\isacharparenright}\ x{\isacharparenright}{\isasymdiv}{\isacharparenright}{\isachardoublequoteclose}% |
1006 \ \ \ \ 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}}% |
1007 \endisatagquote |
1007 \endisatagquote |
1008 {\isafoldquote}% |
1008 {\isafoldquote}% |
1009 % |
1009 % |
1010 \isadelimquote |
1010 \isadelimquote |
1011 % |
1011 % |
1012 \endisadelimquote |
1012 \endisadelimquote |
1013 % |
1013 % |
1014 \begin{isamarkuptext}% |
1014 \begin{isamarkuptext}% |
1015 \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}}.% |
1015 \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}}}.% |
1016 \end{isamarkuptext}% |
1016 \end{isamarkuptext}% |
1017 \isamarkuptrue% |
1017 \isamarkuptrue% |
1018 % |
1018 % |
1019 \isamarkupsubsection{A note on syntax% |
1019 \isamarkupsubsection{A note on syntax% |
1020 } |
1020 } |
1128 \endisadelimquotetypewriter |
1128 \endisadelimquotetypewriter |
1129 % |
1129 % |
1130 \isatagquotetypewriter |
1130 \isatagquotetypewriter |
1131 % |
1131 % |
1132 \begin{isamarkuptext}% |
1132 \begin{isamarkuptext}% |
1133 module\ Example\ where\ {\isacharbraceleft}\isanewline |
1133 module\ Example\ where\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline |
1134 \isanewline |
1134 \isanewline |
1135 data\ Nat\ {\isacharequal}\ Zero{\isacharunderscore}nat\ {\isacharbar}\ Suc\ Nat{\isacharsemicolon}\isanewline |
1135 data\ Nat\ {\isaliteral{3D}{\isacharequal}}\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{7C}{\isacharbar}}\ Suc\ Nat{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
1136 \isanewline |
1136 \isanewline |
1137 nat{\isacharunderscore}aux\ {\isacharcolon}{\isacharcolon}\ Integer\ {\isacharminus}{\isachargreater}\ Nat\ {\isacharminus}{\isachargreater}\ Nat{\isacharsemicolon}\isanewline |
1137 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 |
1138 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 |
1138 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 |
1139 \isanewline |
1139 \isanewline |
1140 nat\ {\isacharcolon}{\isacharcolon}\ Integer\ {\isacharminus}{\isachargreater}\ Nat{\isacharsemicolon}\isanewline |
1140 nat\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ Integer\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ Nat{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
1141 nat\ i\ {\isacharequal}\ nat{\isacharunderscore}aux\ i\ Zero{\isacharunderscore}nat{\isacharsemicolon}\isanewline |
1141 nat\ i\ {\isaliteral{3D}{\isacharequal}}\ nat{\isaliteral{5F}{\isacharunderscore}}aux\ i\ Zero{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
1142 \isanewline |
1142 \isanewline |
1143 class\ Semigroup\ a\ where\ {\isacharbraceleft}\isanewline |
1143 class\ Semigroup\ a\ where\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline |
1144 \ \ mult\ {\isacharcolon}{\isacharcolon}\ a\ {\isacharminus}{\isachargreater}\ a\ {\isacharminus}{\isachargreater}\ a{\isacharsemicolon}\isanewline |
1144 \ \ 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 |
1145 {\isacharbraceright}{\isacharsemicolon}\isanewline |
1145 {\isaliteral{7D}{\isacharbraceright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
1146 \isanewline |
1146 \isanewline |
1147 class\ {\isacharparenleft}Semigroup\ a{\isacharparenright}\ {\isacharequal}{\isachargreater}\ Monoidl\ a\ where\ {\isacharbraceleft}\isanewline |
1147 class\ {\isaliteral{28}{\isacharparenleft}}Semigroup\ a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ Monoidl\ a\ where\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline |
1148 \ \ neutral\ {\isacharcolon}{\isacharcolon}\ a{\isacharsemicolon}\isanewline |
1148 \ \ neutral\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ a{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
1149 {\isacharbraceright}{\isacharsemicolon}\isanewline |
1149 {\isaliteral{7D}{\isacharbraceright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
1150 \isanewline |
1150 \isanewline |
1151 class\ {\isacharparenleft}Monoidl\ a{\isacharparenright}\ {\isacharequal}{\isachargreater}\ Monoid\ a\ where\ {\isacharbraceleft}\isanewline |
1151 class\ {\isaliteral{28}{\isacharparenleft}}Monoidl\ a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ Monoid\ a\ where\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline |
1152 {\isacharbraceright}{\isacharsemicolon}\isanewline |
1152 {\isaliteral{7D}{\isacharbraceright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
1153 \isanewline |
1153 \isanewline |
1154 class\ {\isacharparenleft}Monoid\ a{\isacharparenright}\ {\isacharequal}{\isachargreater}\ Group\ a\ where\ {\isacharbraceleft}\isanewline |
1154 class\ {\isaliteral{28}{\isacharparenleft}}Monoid\ a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ Group\ a\ where\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline |
1155 \ \ inverse\ {\isacharcolon}{\isacharcolon}\ a\ {\isacharminus}{\isachargreater}\ a{\isacharsemicolon}\isanewline |
1155 \ \ inverse\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ a{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
1156 {\isacharbraceright}{\isacharsemicolon}\isanewline |
1156 {\isaliteral{7D}{\isacharbraceright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
1157 \isanewline |
1157 \isanewline |
1158 pow{\isacharunderscore}nat\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ {\isacharparenleft}Monoid\ a{\isacharparenright}\ {\isacharequal}{\isachargreater}\ Nat\ {\isacharminus}{\isachargreater}\ a\ {\isacharminus}{\isachargreater}\ a{\isacharsemicolon}\isanewline |
1158 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 |
1159 pow{\isacharunderscore}nat\ Zero{\isacharunderscore}nat\ x\ {\isacharequal}\ neutral{\isacharsemicolon}\isanewline |
1159 pow{\isaliteral{5F}{\isacharunderscore}}nat\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\ x\ {\isaliteral{3D}{\isacharequal}}\ neutral{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
1160 pow{\isacharunderscore}nat\ {\isacharparenleft}Suc\ n{\isacharparenright}\ x\ {\isacharequal}\ mult\ x\ {\isacharparenleft}pow{\isacharunderscore}nat\ n\ x{\isacharparenright}{\isacharsemicolon}\isanewline |
1160 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 |
1161 \isanewline |
1161 \isanewline |
1162 pow{\isacharunderscore}int\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ {\isacharparenleft}Group\ a{\isacharparenright}\ {\isacharequal}{\isachargreater}\ Integer\ {\isacharminus}{\isachargreater}\ a\ {\isacharminus}{\isachargreater}\ a{\isacharsemicolon}\isanewline |
1162 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 |
1163 pow{\isacharunderscore}int\ k\ x\ {\isacharequal}\isanewline |
1163 pow{\isaliteral{5F}{\isacharunderscore}}int\ k\ x\ {\isaliteral{3D}{\isacharequal}}\isanewline |
1164 \ \ {\isacharparenleft}if\ {\isadigit{0}}\ {\isacharless}{\isacharequal}\ k\ then\ pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ k{\isacharparenright}\ x\isanewline |
1164 \ \ {\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 |
1165 \ \ \ \ else\ inverse\ {\isacharparenleft}pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ {\isacharparenleft}negate\ k{\isacharparenright}{\isacharparenright}\ x{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline |
1165 \ \ \ \ 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 |
1166 \isanewline |
1166 \isanewline |
1167 mult{\isacharunderscore}int\ {\isacharcolon}{\isacharcolon}\ Integer\ {\isacharminus}{\isachargreater}\ Integer\ {\isacharminus}{\isachargreater}\ Integer{\isacharsemicolon}\isanewline |
1167 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 |
1168 mult{\isacharunderscore}int\ i\ j\ {\isacharequal}\ i\ {\isacharplus}\ j{\isacharsemicolon}\isanewline |
1168 mult{\isaliteral{5F}{\isacharunderscore}}int\ i\ j\ {\isaliteral{3D}{\isacharequal}}\ i\ {\isaliteral{2B}{\isacharplus}}\ j{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
1169 \isanewline |
1169 \isanewline |
1170 instance\ Semigroup\ Integer\ where\ {\isacharbraceleft}\isanewline |
1170 instance\ Semigroup\ Integer\ where\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline |
1171 \ \ mult\ {\isacharequal}\ mult{\isacharunderscore}int{\isacharsemicolon}\isanewline |
1171 \ \ mult\ {\isaliteral{3D}{\isacharequal}}\ mult{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
1172 {\isacharbraceright}{\isacharsemicolon}\isanewline |
1172 {\isaliteral{7D}{\isacharbraceright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
1173 \isanewline |
1173 \isanewline |
1174 neutral{\isacharunderscore}int\ {\isacharcolon}{\isacharcolon}\ Integer{\isacharsemicolon}\isanewline |
1174 neutral{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ Integer{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
1175 neutral{\isacharunderscore}int\ {\isacharequal}\ {\isadigit{0}}{\isacharsemicolon}\isanewline |
1175 neutral{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
1176 \isanewline |
1176 \isanewline |
1177 instance\ Monoidl\ Integer\ where\ {\isacharbraceleft}\isanewline |
1177 instance\ Monoidl\ Integer\ where\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline |
1178 \ \ neutral\ {\isacharequal}\ neutral{\isacharunderscore}int{\isacharsemicolon}\isanewline |
1178 \ \ neutral\ {\isaliteral{3D}{\isacharequal}}\ neutral{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
1179 {\isacharbraceright}{\isacharsemicolon}\isanewline |
1179 {\isaliteral{7D}{\isacharbraceright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
1180 \isanewline |
1180 \isanewline |
1181 instance\ Monoid\ Integer\ where\ {\isacharbraceleft}\isanewline |
1181 instance\ Monoid\ Integer\ where\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline |
1182 {\isacharbraceright}{\isacharsemicolon}\isanewline |
1182 {\isaliteral{7D}{\isacharbraceright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
1183 \isanewline |
1183 \isanewline |
1184 inverse{\isacharunderscore}int\ {\isacharcolon}{\isacharcolon}\ Integer\ {\isacharminus}{\isachargreater}\ Integer{\isacharsemicolon}\isanewline |
1184 inverse{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ Integer\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ Integer{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
1185 inverse{\isacharunderscore}int\ i\ {\isacharequal}\ negate\ i{\isacharsemicolon}\isanewline |
1185 inverse{\isaliteral{5F}{\isacharunderscore}}int\ i\ {\isaliteral{3D}{\isacharequal}}\ negate\ i{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
1186 \isanewline |
1186 \isanewline |
1187 instance\ Group\ Integer\ where\ {\isacharbraceleft}\isanewline |
1187 instance\ Group\ Integer\ where\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline |
1188 \ \ inverse\ {\isacharequal}\ inverse{\isacharunderscore}int{\isacharsemicolon}\isanewline |
1188 \ \ inverse\ {\isaliteral{3D}{\isacharequal}}\ inverse{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
1189 {\isacharbraceright}{\isacharsemicolon}\isanewline |
1189 {\isaliteral{7D}{\isacharbraceright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
1190 \isanewline |
1190 \isanewline |
1191 example\ {\isacharcolon}{\isacharcolon}\ Integer{\isacharsemicolon}\isanewline |
1191 example\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ Integer{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
1192 example\ {\isacharequal}\ pow{\isacharunderscore}int\ {\isadigit{1}}{\isadigit{0}}\ {\isacharparenleft}{\isacharminus}{\isadigit{2}}{\isacharparenright}{\isacharsemicolon}\isanewline |
1192 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 |
1193 \isanewline |
1193 \isanewline |
1194 {\isacharbraceright}\isanewline% |
1194 {\isaliteral{7D}{\isacharbraceright}}\isanewline% |
1195 \end{isamarkuptext}% |
1195 \end{isamarkuptext}% |
1196 \isamarkuptrue% |
1196 \isamarkuptrue% |
1197 % |
1197 % |
1198 \endisatagquotetypewriter |
1198 \endisatagquotetypewriter |
1199 {\isafoldquotetypewriter}% |
1199 {\isafoldquotetypewriter}% |
1212 \endisadelimquotetypewriter |
1212 \endisadelimquotetypewriter |
1213 % |
1213 % |
1214 \isatagquotetypewriter |
1214 \isatagquotetypewriter |
1215 % |
1215 % |
1216 \begin{isamarkuptext}% |
1216 \begin{isamarkuptext}% |
1217 structure\ Example\ {\isacharcolon}\ sig\isanewline |
1217 structure\ Example\ {\isaliteral{3A}{\isacharcolon}}\ sig\isanewline |
1218 \ \ datatype\ nat\ {\isacharequal}\ Zero{\isacharunderscore}nat\ {\isacharbar}\ Suc\ of\ nat\isanewline |
1218 \ \ datatype\ nat\ {\isaliteral{3D}{\isacharequal}}\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{7C}{\isacharbar}}\ Suc\ of\ nat\isanewline |
1219 \ \ val\ nat{\isacharunderscore}aux\ {\isacharcolon}\ IntInf{\isachardot}int\ {\isacharminus}{\isachargreater}\ nat\ {\isacharminus}{\isachargreater}\ nat\isanewline |
1219 \ \ 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 |
1220 \ \ val\ nat\ {\isacharcolon}\ IntInf{\isachardot}int\ {\isacharminus}{\isachargreater}\ nat\isanewline |
1220 \ \ val\ nat\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ nat\isanewline |
1221 \ \ type\ {\isacharprime}a\ semigroup\isanewline |
1221 \ \ type\ {\isaliteral{27}{\isacharprime}}a\ semigroup\isanewline |
1222 \ \ val\ mult\ {\isacharcolon}\ {\isacharprime}a\ semigroup\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\isanewline |
1222 \ \ 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 |
1223 \ \ type\ {\isacharprime}a\ monoidl\isanewline |
1223 \ \ type\ {\isaliteral{27}{\isacharprime}}a\ monoidl\isanewline |
1224 \ \ val\ semigroup{\isacharunderscore}monoidl\ {\isacharcolon}\ {\isacharprime}a\ monoidl\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ semigroup\isanewline |
1224 \ \ 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 |
1225 \ \ val\ neutral\ {\isacharcolon}\ {\isacharprime}a\ monoidl\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\isanewline |
1225 \ \ val\ neutral\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ monoidl\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\isanewline |
1226 \ \ type\ {\isacharprime}a\ monoid\isanewline |
1226 \ \ type\ {\isaliteral{27}{\isacharprime}}a\ monoid\isanewline |
1227 \ \ val\ monoidl{\isacharunderscore}monoid\ {\isacharcolon}\ {\isacharprime}a\ monoid\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ monoidl\isanewline |
1227 \ \ 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 |
1228 \ \ type\ {\isacharprime}a\ group\isanewline |
1228 \ \ type\ {\isaliteral{27}{\isacharprime}}a\ group\isanewline |
1229 \ \ val\ monoid{\isacharunderscore}group\ {\isacharcolon}\ {\isacharprime}a\ group\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ monoid\isanewline |
1229 \ \ 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 |
1230 \ \ val\ inverse\ {\isacharcolon}\ {\isacharprime}a\ group\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\isanewline |
1230 \ \ 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 |
1231 \ \ val\ pow{\isacharunderscore}nat\ {\isacharcolon}\ {\isacharprime}a\ monoid\ {\isacharminus}{\isachargreater}\ nat\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\isanewline |
1231 \ \ 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 |
1232 \ \ val\ pow{\isacharunderscore}int\ {\isacharcolon}\ {\isacharprime}a\ group\ {\isacharminus}{\isachargreater}\ IntInf{\isachardot}int\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\isanewline |
1232 \ \ 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 |
1233 \ \ val\ mult{\isacharunderscore}int\ {\isacharcolon}\ IntInf{\isachardot}int\ {\isacharminus}{\isachargreater}\ IntInf{\isachardot}int\ {\isacharminus}{\isachargreater}\ IntInf{\isachardot}int\isanewline |
1233 \ \ 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 |
1234 \ \ val\ semigroup{\isacharunderscore}int\ {\isacharcolon}\ IntInf{\isachardot}int\ semigroup\isanewline |
1234 \ \ val\ semigroup{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ semigroup\isanewline |
1235 \ \ val\ neutral{\isacharunderscore}int\ {\isacharcolon}\ IntInf{\isachardot}int\isanewline |
1235 \ \ val\ neutral{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\isanewline |
1236 \ \ val\ monoidl{\isacharunderscore}int\ {\isacharcolon}\ IntInf{\isachardot}int\ monoidl\isanewline |
1236 \ \ val\ monoidl{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ monoidl\isanewline |
1237 \ \ val\ monoid{\isacharunderscore}int\ {\isacharcolon}\ IntInf{\isachardot}int\ monoid\isanewline |
1237 \ \ val\ monoid{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ monoid\isanewline |
1238 \ \ val\ inverse{\isacharunderscore}int\ {\isacharcolon}\ IntInf{\isachardot}int\ {\isacharminus}{\isachargreater}\ IntInf{\isachardot}int\isanewline |
1238 \ \ 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 |
1239 \ \ val\ group{\isacharunderscore}int\ {\isacharcolon}\ IntInf{\isachardot}int\ group\isanewline |
1239 \ \ val\ group{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ group\isanewline |
1240 \ \ val\ example\ {\isacharcolon}\ IntInf{\isachardot}int\isanewline |
1240 \ \ val\ example\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\isanewline |
1241 end\ {\isacharequal}\ struct\isanewline |
1241 end\ {\isaliteral{3D}{\isacharequal}}\ struct\isanewline |
1242 \isanewline |
1242 \isanewline |
1243 datatype\ nat\ {\isacharequal}\ Zero{\isacharunderscore}nat\ {\isacharbar}\ Suc\ of\ nat{\isacharsemicolon}\isanewline |
1243 datatype\ nat\ {\isaliteral{3D}{\isacharequal}}\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{7C}{\isacharbar}}\ Suc\ of\ nat{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
1244 \isanewline |
1244 \isanewline |
1245 fun\ nat{\isacharunderscore}aux\ i\ n\ {\isacharequal}\isanewline |
1245 fun\ nat{\isaliteral{5F}{\isacharunderscore}}aux\ i\ n\ {\isaliteral{3D}{\isacharequal}}\isanewline |
1246 \ \ {\isacharparenleft}if\ IntInf{\isachardot}{\isacharless}{\isacharequal}\ {\isacharparenleft}i{\isacharcomma}\ {\isacharparenleft}{\isadigit{0}}\ {\isacharcolon}\ IntInf{\isachardot}int{\isacharparenright}{\isacharparenright}\ then\ n\isanewline |
1246 \ \ {\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 |
1247 \ \ \ \ 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 |
1247 \ \ \ \ 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 |
1248 \isanewline |
1248 \isanewline |
1249 fun\ nat\ i\ {\isacharequal}\ nat{\isacharunderscore}aux\ i\ Zero{\isacharunderscore}nat{\isacharsemicolon}\isanewline |
1249 fun\ nat\ i\ {\isaliteral{3D}{\isacharequal}}\ nat{\isaliteral{5F}{\isacharunderscore}}aux\ i\ Zero{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
1250 \isanewline |
1250 \isanewline |
1251 type\ {\isacharprime}a\ semigroup\ {\isacharequal}\ {\isacharbraceleft}mult\ {\isacharcolon}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a{\isacharbraceright}{\isacharsemicolon}\isanewline |
1251 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 |
1252 val\ mult\ {\isacharequal}\ {\isacharhash}mult\ {\isacharcolon}\ {\isacharprime}a\ semigroup\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a{\isacharsemicolon}\isanewline |
1252 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 |
1253 \isanewline |
1253 \isanewline |
1254 type\ {\isacharprime}a\ monoidl\ {\isacharequal}\ {\isacharbraceleft}semigroup{\isacharunderscore}monoidl\ {\isacharcolon}\ {\isacharprime}a\ semigroup{\isacharcomma}\ neutral\ {\isacharcolon}\ {\isacharprime}a{\isacharbraceright}{\isacharsemicolon}\isanewline |
1254 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 |
1255 val\ semigroup{\isacharunderscore}monoidl\ {\isacharequal}\ {\isacharhash}semigroup{\isacharunderscore}monoidl\ {\isacharcolon}\ {\isacharprime}a\ monoidl\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ semigroup{\isacharsemicolon}\isanewline |
1255 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 |
1256 val\ neutral\ {\isacharequal}\ {\isacharhash}neutral\ {\isacharcolon}\ {\isacharprime}a\ monoidl\ {\isacharminus}{\isachargreater}\ {\isacharprime}a{\isacharsemicolon}\isanewline |
1256 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 |
1257 \isanewline |
1257 \isanewline |
1258 type\ {\isacharprime}a\ monoid\ {\isacharequal}\ {\isacharbraceleft}monoidl{\isacharunderscore}monoid\ {\isacharcolon}\ {\isacharprime}a\ monoidl{\isacharbraceright}{\isacharsemicolon}\isanewline |
1258 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 |
1259 val\ monoidl{\isacharunderscore}monoid\ {\isacharequal}\ {\isacharhash}monoidl{\isacharunderscore}monoid\ {\isacharcolon}\ {\isacharprime}a\ monoid\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ monoidl{\isacharsemicolon}\isanewline |
1259 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 |
1260 \isanewline |
1260 \isanewline |
1261 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 |
1261 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 |
1262 val\ monoid{\isacharunderscore}group\ {\isacharequal}\ {\isacharhash}monoid{\isacharunderscore}group\ {\isacharcolon}\ {\isacharprime}a\ group\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ monoid{\isacharsemicolon}\isanewline |
1262 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 |
1263 val\ inverse\ {\isacharequal}\ {\isacharhash}inverse\ {\isacharcolon}\ {\isacharprime}a\ group\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a{\isacharsemicolon}\isanewline |
1263 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 |
1264 \isanewline |
1264 \isanewline |
1265 fun\ pow{\isacharunderscore}nat\ A{\isacharunderscore}\ Zero{\isacharunderscore}nat\ x\ {\isacharequal}\ neutral\ {\isacharparenleft}monoidl{\isacharunderscore}monoid\ A{\isacharunderscore}{\isacharparenright}\isanewline |
1265 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 |
1266 \ \ {\isacharbar}\ pow{\isacharunderscore}nat\ A{\isacharunderscore}\ {\isacharparenleft}Suc\ n{\isacharparenright}\ x\ {\isacharequal}\isanewline |
1266 \ \ {\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 |
1267 \ \ \ \ 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 |
1267 \ \ \ \ 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 |
1268 \isanewline |
1268 \isanewline |
1269 fun\ pow{\isacharunderscore}int\ A{\isacharunderscore}\ k\ x\ {\isacharequal}\isanewline |
1269 fun\ pow{\isaliteral{5F}{\isacharunderscore}}int\ A{\isaliteral{5F}{\isacharunderscore}}\ k\ x\ {\isaliteral{3D}{\isacharequal}}\isanewline |
1270 \ \ {\isacharparenleft}if\ IntInf{\isachardot}{\isacharless}{\isacharequal}\ {\isacharparenleft}{\isacharparenleft}{\isadigit{0}}\ {\isacharcolon}\ IntInf{\isachardot}int{\isacharparenright}{\isacharcomma}\ k{\isacharparenright}\isanewline |
1270 \ \ {\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 |
1271 \ \ \ \ then\ pow{\isacharunderscore}nat\ {\isacharparenleft}monoid{\isacharunderscore}group\ A{\isacharunderscore}{\isacharparenright}\ {\isacharparenleft}nat\ k{\isacharparenright}\ x\isanewline |
1271 \ \ \ \ 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 |
1272 \ \ \ \ 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 |
1272 \ \ \ \ 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 |
1273 \isanewline |
1273 \isanewline |
1274 fun\ mult{\isacharunderscore}int\ i\ j\ {\isacharequal}\ IntInf{\isachardot}{\isacharplus}\ {\isacharparenleft}i{\isacharcomma}\ j{\isacharparenright}{\isacharsemicolon}\isanewline |
1274 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 |
1275 \isanewline |
1275 \isanewline |
1276 val\ semigroup{\isacharunderscore}int\ {\isacharequal}\ {\isacharbraceleft}mult\ {\isacharequal}\ mult{\isacharunderscore}int{\isacharbraceright}\ {\isacharcolon}\ IntInf{\isachardot}int\ semigroup{\isacharsemicolon}\isanewline |
1276 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 |
1277 \isanewline |
1277 \isanewline |
1278 val\ neutral{\isacharunderscore}int\ {\isacharcolon}\ IntInf{\isachardot}int\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}\ {\isacharcolon}\ IntInf{\isachardot}int{\isacharparenright}{\isacharsemicolon}\isanewline |
1278 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 |
1279 \isanewline |
1279 \isanewline |
1280 val\ monoidl{\isacharunderscore}int\ {\isacharequal}\isanewline |
1280 val\ monoidl{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3D}{\isacharequal}}\isanewline |
1281 \ \ {\isacharbraceleft}semigroup{\isacharunderscore}monoidl\ {\isacharequal}\ semigroup{\isacharunderscore}int{\isacharcomma}\ neutral\ {\isacharequal}\ neutral{\isacharunderscore}int{\isacharbraceright}\ {\isacharcolon}\isanewline |
1281 \ \ {\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 |
1282 \ \ IntInf{\isachardot}int\ monoidl{\isacharsemicolon}\isanewline |
1282 \ \ IntInf{\isaliteral{2E}{\isachardot}}int\ monoidl{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
1283 \isanewline |
1283 \isanewline |
1284 val\ monoid{\isacharunderscore}int\ {\isacharequal}\ {\isacharbraceleft}monoidl{\isacharunderscore}monoid\ {\isacharequal}\ monoidl{\isacharunderscore}int{\isacharbraceright}\ {\isacharcolon}\ IntInf{\isachardot}int\ monoid{\isacharsemicolon}\isanewline |
1284 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 |
1285 \isanewline |
1285 \isanewline |
1286 fun\ inverse{\isacharunderscore}int\ i\ {\isacharequal}\ IntInf{\isachardot}{\isachartilde}\ i{\isacharsemicolon}\isanewline |
1286 fun\ inverse{\isaliteral{5F}{\isacharunderscore}}int\ i\ {\isaliteral{3D}{\isacharequal}}\ IntInf{\isaliteral{2E}{\isachardot}}{\isaliteral{7E}{\isachartilde}}\ i{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
1287 \isanewline |
1287 \isanewline |
1288 val\ group{\isacharunderscore}int\ {\isacharequal}\ {\isacharbraceleft}monoid{\isacharunderscore}group\ {\isacharequal}\ monoid{\isacharunderscore}int{\isacharcomma}\ inverse\ {\isacharequal}\ inverse{\isacharunderscore}int{\isacharbraceright}\ {\isacharcolon}\isanewline |
1288 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 |
1289 \ \ IntInf{\isachardot}int\ group{\isacharsemicolon}\isanewline |
1289 \ \ IntInf{\isaliteral{2E}{\isachardot}}int\ group{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
1290 \isanewline |
1290 \isanewline |
1291 val\ example\ {\isacharcolon}\ IntInf{\isachardot}int\ {\isacharequal}\isanewline |
1291 val\ example\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ {\isaliteral{3D}{\isacharequal}}\isanewline |
1292 \ \ 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 |
1292 \ \ 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 |
1293 \isanewline |
1293 \isanewline |
1294 end{\isacharsemicolon}\ {\isacharparenleft}{\isacharasterisk}struct\ Example{\isacharasterisk}{\isacharparenright}\isanewline% |
1294 end{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}struct\ Example{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline% |
1295 \end{isamarkuptext}% |
1295 \end{isamarkuptext}% |
1296 \isamarkuptrue% |
1296 \isamarkuptrue% |
1297 % |
1297 % |
1298 \endisatagquotetypewriter |
1298 \endisatagquotetypewriter |
1299 {\isafoldquotetypewriter}% |
1299 {\isafoldquotetypewriter}% |
1325 \endisadelimquotetypewriter |
1325 \endisadelimquotetypewriter |
1326 % |
1326 % |
1327 \isatagquotetypewriter |
1327 \isatagquotetypewriter |
1328 % |
1328 % |
1329 \begin{isamarkuptext}% |
1329 \begin{isamarkuptext}% |
1330 object\ Example\ {\isacharbraceleft}\isanewline |
1330 object\ Example\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline |
1331 \isanewline |
1331 \isanewline |
1332 abstract\ sealed\ class\ nat\isanewline |
1332 abstract\ sealed\ class\ nat\isanewline |
1333 final\ case\ object\ Zero{\isacharunderscore}nat\ extends\ nat\isanewline |
1333 final\ case\ object\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\ extends\ nat\isanewline |
1334 final\ case\ class\ Suc{\isacharparenleft}a{\isacharcolon}\ nat{\isacharparenright}\ extends\ nat\isanewline |
1334 final\ case\ class\ Suc{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{3A}{\isacharcolon}}\ nat{\isaliteral{29}{\isacharparenright}}\ extends\ nat\isanewline |
1335 \isanewline |
1335 \isanewline |
1336 def\ nat{\isacharunderscore}aux{\isacharparenleft}i{\isacharcolon}\ BigInt{\isacharcomma}\ n{\isacharcolon}\ nat{\isacharparenright}{\isacharcolon}\ nat\ {\isacharequal}\isanewline |
1336 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 |
1337 \ \ {\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 |
1337 \ \ {\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 |
1338 \isanewline |
1338 \isanewline |
1339 def\ nat{\isacharparenleft}i{\isacharcolon}\ BigInt{\isacharparenright}{\isacharcolon}\ nat\ {\isacharequal}\ nat{\isacharunderscore}aux{\isacharparenleft}i{\isacharcomma}\ Zero{\isacharunderscore}nat{\isacharparenright}\isanewline |
1339 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 |
1340 \isanewline |
1340 \isanewline |
1341 trait\ semigroup{\isacharbrackleft}A{\isacharbrackright}\ {\isacharbraceleft}\isanewline |
1341 trait\ semigroup{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline |
1342 \ \ val\ {\isacharbackquote}Example{\isachardot}mult{\isacharbackquote}{\isacharcolon}\ {\isacharparenleft}A{\isacharcomma}\ A{\isacharparenright}\ {\isacharequal}{\isachargreater}\ A\isanewline |
1342 \ \ 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 |
1343 {\isacharbraceright}\isanewline |
1343 {\isaliteral{7D}{\isacharbraceright}}\isanewline |
1344 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 |
1344 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 |
1345 \ \ A{\isachardot}{\isacharbackquote}Example{\isachardot}mult{\isacharbackquote}{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\isanewline |
1345 \ \ 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 |
1346 \isanewline |
1346 \isanewline |
1347 trait\ monoidl{\isacharbrackleft}A{\isacharbrackright}\ extends\ semigroup{\isacharbrackleft}A{\isacharbrackright}\ {\isacharbraceleft}\isanewline |
1347 trait\ monoidl{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}\ extends\ semigroup{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline |
1348 \ \ val\ {\isacharbackquote}Example{\isachardot}neutral{\isacharbackquote}{\isacharcolon}\ A\isanewline |
1348 \ \ val\ {\isaliteral{60}{\isacharbackquote}}Example{\isaliteral{2E}{\isachardot}}neutral{\isaliteral{60}{\isacharbackquote}}{\isaliteral{3A}{\isacharcolon}}\ A\isanewline |
1349 {\isacharbraceright}\isanewline |
1349 {\isaliteral{7D}{\isacharbraceright}}\isanewline |
1350 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 |
1350 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 |
1351 \isanewline |
1351 \isanewline |
1352 trait\ monoid{\isacharbrackleft}A{\isacharbrackright}\ extends\ monoidl{\isacharbrackleft}A{\isacharbrackright}\ {\isacharbraceleft}\isanewline |
1352 trait\ monoid{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}\ extends\ monoidl{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline |
1353 {\isacharbraceright}\isanewline |
1353 {\isaliteral{7D}{\isacharbraceright}}\isanewline |
1354 \isanewline |
1354 \isanewline |
1355 trait\ group{\isacharbrackleft}A{\isacharbrackright}\ extends\ monoid{\isacharbrackleft}A{\isacharbrackright}\ {\isacharbraceleft}\isanewline |
1355 trait\ group{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}\ extends\ monoid{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline |
1356 \ \ val\ {\isacharbackquote}Example{\isachardot}inverse{\isacharbackquote}{\isacharcolon}\ A\ {\isacharequal}{\isachargreater}\ A\isanewline |
1356 \ \ val\ {\isaliteral{60}{\isacharbackquote}}Example{\isaliteral{2E}{\isachardot}}inverse{\isaliteral{60}{\isacharbackquote}}{\isaliteral{3A}{\isacharcolon}}\ A\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ A\isanewline |
1357 {\isacharbraceright}\isanewline |
1357 {\isaliteral{7D}{\isacharbraceright}}\isanewline |
1358 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 |
1358 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 |
1359 \isanewline |
1359 \isanewline |
1360 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 |
1360 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 |
1361 \ \ case\ {\isacharparenleft}Zero{\isacharunderscore}nat{\isacharcomma}\ x{\isacharparenright}\ {\isacharequal}{\isachargreater}\ neutral{\isacharbrackleft}A{\isacharbrackright}\isanewline |
1361 \ \ 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 |
1362 \ \ 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 |
1362 \ \ 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 |
1363 {\isacharbraceright}\isanewline |
1363 {\isaliteral{7D}{\isacharbraceright}}\isanewline |
1364 \isanewline |
1364 \isanewline |
1365 def\ pow{\isacharunderscore}int{\isacharbrackleft}A{\isacharcolon}\ group{\isacharbrackright}{\isacharparenleft}k{\isacharcolon}\ BigInt{\isacharcomma}\ x{\isacharcolon}\ A{\isacharparenright}{\isacharcolon}\ A\ {\isacharequal}\isanewline |
1365 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 |
1366 \ \ {\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 |
1366 \ \ {\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 |
1367 \ \ \ \ 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 |
1367 \ \ \ \ 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 |
1368 \isanewline |
1368 \isanewline |
1369 def\ mult{\isacharunderscore}int{\isacharparenleft}i{\isacharcolon}\ BigInt{\isacharcomma}\ j{\isacharcolon}\ BigInt{\isacharparenright}{\isacharcolon}\ BigInt\ {\isacharequal}\ i\ {\isacharplus}\ j\isanewline |
1369 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 |
1370 \isanewline |
1370 \isanewline |
1371 implicit\ def\ semigroup{\isacharunderscore}int{\isacharcolon}\ semigroup{\isacharbrackleft}BigInt{\isacharbrackright}\ {\isacharequal}\ new\ semigroup{\isacharbrackleft}BigInt{\isacharbrackright}\ {\isacharbraceleft}\isanewline |
1371 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 |
1372 \ \ 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 |
1372 \ \ 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 |
1373 {\isacharbraceright}\isanewline |
1373 {\isaliteral{7D}{\isacharbraceright}}\isanewline |
1374 \isanewline |
1374 \isanewline |
1375 def\ neutral{\isacharunderscore}int{\isacharcolon}\ BigInt\ {\isacharequal}\ BigInt{\isacharparenleft}{\isadigit{0}}{\isacharparenright}\isanewline |
1375 def\ neutral{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{3A}{\isacharcolon}}\ BigInt\ {\isaliteral{3D}{\isacharequal}}\ BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline |
1376 \isanewline |
1376 \isanewline |
1377 implicit\ def\ monoidl{\isacharunderscore}int{\isacharcolon}\ monoidl{\isacharbrackleft}BigInt{\isacharbrackright}\ {\isacharequal}\ new\ monoidl{\isacharbrackleft}BigInt{\isacharbrackright}\ {\isacharbraceleft}\isanewline |
1377 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 |
1378 \ \ val\ {\isacharbackquote}Example{\isachardot}neutral{\isacharbackquote}\ {\isacharequal}\ neutral{\isacharunderscore}int\isanewline |
1378 \ \ val\ {\isaliteral{60}{\isacharbackquote}}Example{\isaliteral{2E}{\isachardot}}neutral{\isaliteral{60}{\isacharbackquote}}\ {\isaliteral{3D}{\isacharequal}}\ neutral{\isaliteral{5F}{\isacharunderscore}}int\isanewline |
1379 \ \ 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 |
1379 \ \ 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 |
1380 {\isacharbraceright}\isanewline |
1380 {\isaliteral{7D}{\isacharbraceright}}\isanewline |
1381 \isanewline |
1381 \isanewline |
1382 implicit\ def\ monoid{\isacharunderscore}int{\isacharcolon}\ monoid{\isacharbrackleft}BigInt{\isacharbrackright}\ {\isacharequal}\ new\ monoid{\isacharbrackleft}BigInt{\isacharbrackright}\ {\isacharbraceleft}\isanewline |
1382 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 |
1383 \ \ val\ {\isacharbackquote}Example{\isachardot}neutral{\isacharbackquote}\ {\isacharequal}\ neutral{\isacharunderscore}int\isanewline |
1383 \ \ val\ {\isaliteral{60}{\isacharbackquote}}Example{\isaliteral{2E}{\isachardot}}neutral{\isaliteral{60}{\isacharbackquote}}\ {\isaliteral{3D}{\isacharequal}}\ neutral{\isaliteral{5F}{\isacharunderscore}}int\isanewline |
1384 \ \ 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 |
1384 \ \ 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 |
1385 {\isacharbraceright}\isanewline |
1385 {\isaliteral{7D}{\isacharbraceright}}\isanewline |
1386 \isanewline |
1386 \isanewline |
1387 def\ inverse{\isacharunderscore}int{\isacharparenleft}i{\isacharcolon}\ BigInt{\isacharparenright}{\isacharcolon}\ BigInt\ {\isacharequal}\ {\isacharparenleft}{\isacharminus}\ i{\isacharparenright}\isanewline |
1387 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 |
1388 \isanewline |
1388 \isanewline |
1389 implicit\ def\ group{\isacharunderscore}int{\isacharcolon}\ group{\isacharbrackleft}BigInt{\isacharbrackright}\ {\isacharequal}\ new\ group{\isacharbrackleft}BigInt{\isacharbrackright}\ {\isacharbraceleft}\isanewline |
1389 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 |
1390 \ \ val\ {\isacharbackquote}Example{\isachardot}inverse{\isacharbackquote}\ {\isacharequal}\ {\isacharparenleft}a{\isacharcolon}\ BigInt{\isacharparenright}\ {\isacharequal}{\isachargreater}\ inverse{\isacharunderscore}int{\isacharparenleft}a{\isacharparenright}\isanewline |
1390 \ \ 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 |
1391 \ \ val\ {\isacharbackquote}Example{\isachardot}neutral{\isacharbackquote}\ {\isacharequal}\ neutral{\isacharunderscore}int\isanewline |
1391 \ \ val\ {\isaliteral{60}{\isacharbackquote}}Example{\isaliteral{2E}{\isachardot}}neutral{\isaliteral{60}{\isacharbackquote}}\ {\isaliteral{3D}{\isacharequal}}\ neutral{\isaliteral{5F}{\isacharunderscore}}int\isanewline |
1392 \ \ 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 |
1392 \ \ 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 |
1393 {\isacharbraceright}\isanewline |
1393 {\isaliteral{7D}{\isacharbraceright}}\isanewline |
1394 \isanewline |
1394 \isanewline |
1395 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 |
1395 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 |
1396 \isanewline |
1396 \isanewline |
1397 {\isacharbraceright}\ {\isacharslash}{\isacharasterisk}\ object\ Example\ {\isacharasterisk}{\isacharslash}\isanewline% |
1397 {\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{2F}{\isacharslash}}{\isaliteral{2A}{\isacharasterisk}}\ object\ Example\ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{2F}{\isacharslash}}\isanewline% |
1398 \end{isamarkuptext}% |
1398 \end{isamarkuptext}% |
1399 \isamarkuptrue% |
1399 \isamarkuptrue% |
1400 % |
1400 % |
1401 \endisatagquotetypewriter |
1401 \endisatagquotetypewriter |
1402 {\isafoldquotetypewriter}% |
1402 {\isafoldquotetypewriter}% |