\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
