diff options
Diffstat (limited to 'macros/latex/contrib/stex/doc/packages/stex-statements.tex')
-rw-r--r-- | macros/latex/contrib/stex/doc/packages/stex-statements.tex | 145 |
1 files changed, 0 insertions, 145 deletions
diff --git a/macros/latex/contrib/stex/doc/packages/stex-statements.tex b/macros/latex/contrib/stex/doc/packages/stex-statements.tex deleted file mode 100644 index 6a2478fa7d..0000000000 --- a/macros/latex/contrib/stex/doc/packages/stex-statements.tex +++ /dev/null @@ -1,145 +0,0 @@ -\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 |