diff options
author | Karl Berry <karl@freefriends.org> | 2022-05-24 20:23:29 +0000 |
---|---|---|
committer | Karl Berry <karl@freefriends.org> | 2022-05-24 20:23:29 +0000 |
commit | d1a45dc92e84130c08386511a72d4ba1bc95b1b9 (patch) | |
tree | 0b41d5e406b7fb349d9c8a6fe3e05e255e2b92a9 /Master/texmf-dist/doc/latex/stex/packages/stex-statements.tex | |
parent | 36e380761892b6ddfed9ad4e5cd585a8b3ae17cc (diff) |
stex (24may22)
git-svn-id: svn://tug.org/texlive/trunk@63390 c570f23f-e606-0410-a88d-b1316a301751
Diffstat (limited to 'Master/texmf-dist/doc/latex/stex/packages/stex-statements.tex')
-rw-r--r-- | Master/texmf-dist/doc/latex/stex/packages/stex-statements.tex | 146 |
1 files changed, 145 insertions, 1 deletions
diff --git a/Master/texmf-dist/doc/latex/stex/packages/stex-statements.tex b/Master/texmf-dist/doc/latex/stex/packages/stex-statements.tex index aa9f5f76abf..6a2478fa7d1 100644 --- a/Master/texmf-dist/doc/latex/stex/packages/stex-statements.tex +++ b/Master/texmf-dist/doc/latex/stex/packages/stex-statements.tex @@ -1 +1,145 @@ -\textcolor{red}{TODO: statements documentation}
\ No newline at end of file +\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 |