summaryrefslogtreecommitdiff
path: root/macros/latex/contrib/stex/doc/packages/stex-statements.tex
diff options
context:
space:
mode:
Diffstat (limited to 'macros/latex/contrib/stex/doc/packages/stex-statements.tex')
-rw-r--r--macros/latex/contrib/stex/doc/packages/stex-statements.tex145
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