1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
|
\begin{sfragment}{Definitions, Theorems, Examples, Paragraphs}
\begin{smodule}{Statements}
As mentioned earlier, we can semantically mark-up
\emph{statements} such as definitions, theorems, lemmata, examples, etc.
The corresponding environments for that are:
\begin{itemize}
\item \stexcode"sdefinition" for definitions,
\item \stexcode"sassertion" for assertions, i.e.
propositions that are declared to be \emph{true},
such as theorems, lemmata, axioms,
\item \stexcode"sexample" for examples and counterexamples, and
\item \stexcode"sparagraph" for ``other'' semantic paragraphs,
such as comments, remarks, conjectures, etc.
\end{itemize}
The \emph{presentation} of these environments can be customized
to use e.g. predefined |theorem|-environments, see \sref{sec.customhighlight}
for details.
All of these environments take optional arguments in the form of
|key=value|-pairs. Common to all of them are the keys |id=| (for cross-referencing,
see \sref{sec.references}), |type=| for customization (see \sref{sec.customhighlight})
and additional information (e.g. definition principles, ``difficulty'' etc), as well
as |title=| (for giving the paragraph a title), and finally |for=|.
The |for=| key expects a comma-separated list of existing
symbols, allowing for e.g. things like
\symdef{addition}[args=a,prec=100]{#1}{##1 \comp+ ##2}
\symdef{multiplication}[args=a,prec=50]{#1}{##1 \comp\cdot ##2}
\stexexample{%
\begin{sexample}[
id=additionandmultiplication.ex,
for={addition,multiplication},
type={trivial,boring},
title={An Example}
]
$\addition{2,3}$ is $5$, $\multiplication{2,3}$ is $6$.
\end{sexample}
}
\begin{function}{\definiendum,\definame,\Definame}
\stexcode"sdefinition" (and \stexcode"sparagraph" with
|type=symdoc|) introduce three new macros:
\stexcode"definiendum" behaves like \stexcode"symref"
(and \stexcode"definame"/\stexcode"Definame"
like \stexcode"symname"/\stexcode"Symname", respectively),
but highlights the referenced symbol as \emph{being defined}
in the current definition.
\end{function}
\begin{mmtbox}
The special |type=symdoc| for \stexcode"sparagraph" is intended to be used for
``informal definitions'', or encyclopedia-style descriptions for symbols.
The \mmt system can use those (in lieu of an actual \stexcode"sdefinition" in scope)
to present to users, e.g. when hovering over symbols.
\end{mmtbox}
\begin{function}{\definiens}
Additionally, \stexcode"sdefinition" (and \stexcode"sparagraph" with
|type=symdoc|) introduces \stexcode"\definiens[<optional symbolname>]{<code>}"
which marks up |<code>| as being the explicit \emph{definiens}
of |<optional symbolname>| (in case |for=| has multiple symbols).
\end{function}
All four statement environments -- i.e. \stexcode|sdefinition|,
\stexcode|sassertion|, \stexcode|sexample|, and \stexcode|sparagraph| -- also take an
optional parameter |name=| -- if this one is given a value, the environment will
generate a \emph{symbol} by that name (but with no semantic macro). Not only does this
allow for \stexcode"\symref" et al, it allows us to resume our earlier example for
monoids much more nicely:\ednote{MK: we should reference the example explicitly here.}
\symdef{set}{\comp{\texttt{Set}}}
\symdef{equal}[args=2]{#1 \comp= #2}
\symdef{inset}[args=2]{#1 \comp\in #2}
\symdef{funtype}[args=ai]{#1 \comp\to #2}{##1 \comp\times ##2}
\stexexample{%
\begin{mathstructure}{monoid}
\symdef{universe}[type=\set]{\comp{U}}
\symdef{op}[
args=2,
type=\funtype{\universe,\universe}{\universe},
op=\circ
]{#1 \comp{\circ} #2}
\symdef{unit}[type=\universe]{\comp{e}}
\begin{sparagraph}[type=symdoc,for=monoid]
A \definame{monoid} is a structure
$\mathstruct{\universe,\op!,\unit}$
where $\op!:\funtype{\universe}{\universe}$ and
$\inset{\unit}{\universe}$ such that
\begin{sassertion}[name=associative,
type=axiom,
title=Associativity]
$\op!$ is associative
\end{sassertion}
\begin{sassertion}[name=isunit,
type=axiom,
title=Unit]
$\equal{\op{\svar{x}}{\unit}}{\svar{x}}$
for all $\inset{\svar{x}}{\universe}$
\end{sassertion}
\end{sparagraph}
\end{mathstructure}
An example for a \symname{monoid} is...
}
The main difference to before\ednote{MK: reference} is that the two
\stexcode|sassertion|s now have |name=| attributes. Thus the \stexcode"mathstructure"
\symname{monoid} now contains two additional symbols, namely the axioms for
associativity and that $e$ is a unit. Note that both symbols do not represent the mere
\emph{propositions} that e.g. $\circ$ is associative, but \emph{the assertion that it
is actually true} that $\circ$ is associative.
If we now want to instantiate |monoid| (unless with a variable,
of course), we also need to assign |associative| and |neutral|
to analogous assertions. So the earlier example
\begin{latexcode}[gobble=8]
\instantiate{intmonoid}{monoid}{\mathbb{Z}_{+,0}}[
universe = Int ,
op = addition ,
unit = zero
]
\end{latexcode}
...will not work anymore. We now need to give assertions that
|addition| is associative and that |zero| is a unit with respect
to addition.\footnote{Of course, \sTeX can not check that
the assertions are the ``correct'' ones -- but if
the assertions (both in |monoid| as well as those for addition and
zero) are properly marked up, \mmt can. \textcolor{red}{TODO: should}}
\end{smodule}
\end{sfragment}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "../stex-manual"
%%% End:
% LocalWords: sec.customhighlight a,prec additionandmultiplication.ex trivial,boring
% LocalWords: addition,multiplication symdoc symdoc,for isunit
|
