\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[]{}" which marks up || as being the explicit \emph{definiens} of || (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