summaryrefslogtreecommitdiff
path: root/Master/texmf-dist/doc/latex/stex/packages/stex-statements.tex
diff options
context:
space:
mode:
authorKarl Berry <karl@freefriends.org>2022-05-24 20:23:29 +0000
committerKarl Berry <karl@freefriends.org>2022-05-24 20:23:29 +0000
commitd1a45dc92e84130c08386511a72d4ba1bc95b1b9 (patch)
tree0b41d5e406b7fb349d9c8a6fe3e05e255e2b92a9 /Master/texmf-dist/doc/latex/stex/packages/stex-statements.tex
parent36e380761892b6ddfed9ad4e5cd585a8b3ae17cc (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.tex146
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