
Definentia

Using Symbols Without Semantic Macros and Exporting Code in Modules

3.2.2 Assertions

3.2.3 Proofs

3.3 Mathematical Structures

3.3.1 Declaring and Using Structures

3.3.2 Extending Structures and Axioms

3.3.3 Testing Structures and \this

3.4 Complex Inheritance and Theory Morphisms

3.4.1 Glueing Structures Together

3.4.2 Realizations

4 Extensions for Education

4.1 Slides and Course Notes

4.2 Problems and Exercises

4.3 Exams

## II User Manual

* 5 Basics
	* 5.1 Package and Class Options
	* 5.2 Math Archives and the MathHub Directory
		* 5.2.1 The Structure of Math Archives
		* 5.2.2 MANIFEST.MF-Files
	* 5.3 The lib-Directory
	* 5.4 Basic Macros

* 6 Document Features
	* 6.1 Document Fragments
	* 6.2 Using and Referencing Document Fragments
	* 6.3 Cross-Document References

* 7 Modules and Symbols
	* 7.1 Modules
		* 7.1.1 Signature Modules, Languages, and Multilinguality
	* 7.2 Symbol Declarations
		* 7.2.1 Returns
	* 7.3 Referencing Symbols
	* 7.4 Notations and Semantic Macros
		* 7.4.1 Precedences and Bracketing
		* 7.4.2 Notations for Argument Sequences
		* 7.4.3 Semantic Macros
	* 7.5 Simple Inheritance
	* 7.6 Variables and Sequences
	* 7.7 Structures
		* 7.7.1 Semantic Macros for Structures
Statements * 8.1 More on Definitions * 8.2 More on Assertions
* 9 Customizing Typesetting
	* 9.1 Highlighting Symbol References
	* 9.2 Styling Environments and Macros
	* 9.3 Custom CSS for Environments
* 10 Additional Packages
	* 10.1 NotesSlides Manual
		* 10.1.1 Introduction
		* 10.1.2 Package Options
		* 10.1.3 Notes and Slides
		* 10.1.4 Customizing Header and Footer Lines
		* 10.1.5 Frame Images
		* 10.1.6 Ending Documents Prematurely
		* 10.1.7 Global Document Variables
		* 10.1.8 Excursions
	* 10.2 Problem Manual
		* 10.2.1 Introduction
		* 10.2.2 Problems and Solutions
		* 10.2.3 Markup for Added-Value Services
* Multiple Choice Blocks
* Filling-In Concrete Solutions
		* 10.2.4 Including Problems
		* 10.2.5 Testing and Spacing
	* 10.3 HWExam Manual
		* 10.3.1 Introduction
		* 10.3.2 Package Options
		* 10.3.3 Assignments
		* 10.3.4 Including Assignments
		* 10.3.5 Typesetting Exams
	* 10.4 Tikzinput Manual

## 3 Documentation

* 11 SleX Developer Manual
	* 11.1 Documents
	* 11.2 Modules
	* 11.3 Symbols
	* 11.4 Notations
	* 11.5 Structural Features
	* 11.6 Imports and Morphisms
	* 11.7 Expressions and Semantic Macros
	* 11.8 Optional (Key-Value) Argument Handling
	* 11.9 Stylable Commands and Environments
* 11.10 Math Archives
* 11.11 SMS-Mode
11.11.1 Second Pass 124 11.11.2 First Pass 125 11.12 Strings, File Paths, URIs 126 11.12.1 File Paths File Path Constants and Variables 127 11.12.2 URIs 128 11.13 Language Handling 128 11.14 Inserting Annotations 129 11.14.1 Backend macros 129 11.15 Persisting Content from Math Archives in sms-Files 130 11.16 Utility Methods 130 11.16.1 Group-like Behaviours 131
* 12 Additional Packages 133 12.1 NotesSlides Documentation 133 12.2 Problem Documentation 133 12.3 HWExam Documentation 133 12.4 Tikzinput Documentation

## 4 Implementation

* 13 The SLEX Implementation 13.1 Setting up 13.2 Utilities 13.2.1 Calling kpsewhich and Environment Variables 13.2.2 Logging 13.2.3 Languages 13.2.4 Group-like Behaviours 13.2.5 HTML Annotations 13.2.6 Auxiliary Methods 13.2.7 Persistence 13.2.8 Files, Paths and URIs 13.2.9 File Hooks 157 13.3 Math Archives 159 13.4 Documents 13.4.1 Title 13.4.2 Sectioning 13.4.3 References 13.4.4 Inputs 13.5 SMS Mode 13.6 Modules 13.6.1 The smodule-environment 13.6.2 Structural Features 13.7 Inheritance 13.7.1 \importmodule/usemodule 13.7.2 Theory Morphisms 13.8 Symbols 13.8.1 Declarations



### 1.2 The \(\$\mathrm{T}\mathrm{E}\mathrm{X}\) package

The \(\$\mathrm{T}\mathrm{E}\mathrm{X}\) package extends \(\$\mathrm{T}\mathrm{E}\mathrm{X}\) with:

* concepts, functions, relations, variables, etc., which can be used and referenced in text or via semantic macros in mathematical formulae,
* modules bundle declarations, definitions, theorems, document snippets, and symbols for reuse, and
* an analogous organizational structure for developing documents modularly from individual fragments and sections.

The \(\$\mathrm{T}\mathrm{E}\mathrm{X}\) package has been designed to have minimal impact on other packages and document classes, or the actual document layout - formatting of semantic environments, symbol references and semantic macros can be fully customized.

### 1.3 What is \(\mathrm{M}\mathrm{m}\mathrm{t}\)?

\(\mathrm{M}\mathrm{m}\mathrm{t}\) is a software system and \(\mathrm{S}\mathrm{c}\mathrm{a}\mathrm{I}\mathrm{A}\mathrm{P}\) for generic knowledge management services. It is based on a version of the \(\mathrm{O}\mathrm{M}\mathrm{D}\mathrm{o}\mathrm{c}\) ontology and document format (\(\mathrm{M}\mathrm{m}\mathrm{t}\)/\(\mathrm{O}\mathrm{M}\mathrm{D}\mathrm{o}\mathrm{c}\)).

Among the services \(\mathrm{M}\mathrm{m}\mathrm{t}\) provides are compiling, building, converting and managing libraries, a built-in web-server for browsing content, various algorithms for generic computation, checking and translating expressions, and querying.

### 1.4 Math archives and the MathHub Directory

To make the most of \(\$\mathrm{T}\mathrm{E}\mathrm{X}\), it is strongly encouraged to follow a workflow of small document fragments and modules to maximize reuse.

One considerable weakness of \(\$\mathrm{T}\mathrm{E}\mathrm{X}\) is the way source files are referenced: they need to be either in a \(\mathtt{texmf}\) directory, or else be referenced via file paths relative to the main.tex-file being compiled. This is highly inconvenient if we want to collaboratively develop many highly interrelated document fragments.

\(\$\mathrm{T}\mathrm{E}\mathrm{X}\) therefore adds an organizational layer on top of \(\$\mathrm{T}\mathrm{E}\mathrm{X}\)'s: \(\mathtt{math}\)\(\mathtt{archives}\) stored in a fixed \(\mathtt{MathHub}\) directory anywhere on your hard drive. Referencing source files and modules is then done relative to the containing \(\mathtt{math}\)\(\mathtt{archive}\), and is thus _independent_ of user's individual setups or the current.tex-file.

The drawback of this approach is that \(\$\mathrm{T}\mathrm{E}\mathrm{X}\) needs to know the location of \(\mathtt{y}\)\(\mathtt{MathHub}\) directory. There are multiple ways to achieve that, but the simplest and recommended approach is to set an environment variable: Simply create a new directory <path>/\(\mathtt{MathHub}\) somewhere on your hard drive and set the environment variable \(\mathrm{M}\mathrm{T}\mathrm{H}\mathrm{U}\mathrm{B}\) as the path to this new directory.

Alternatively, you can let the \(\$\mathrm{T}\mathrm{E}\mathrm{X}\) IDE do the work for you (see section 1.5).

For more on math archives, see section 5.2.


And that's it. Click on _Finish_ and your setup is finished. The extension will start and download \(\mbox{\sc R}_{\mbox{\sc U}}\mbox{\sc S}_{\mbox{\sc E}}\mbox{\sc X}\) and some fundamental math archives for you automatically (an internet connection is required when finishing the setup).

## Part I Tutorial

_The dynamic HTML version of this part can be found at_

[https://stexmmt.mathhub.info/](https://stexmmt.mathhub.info/):

sTeX/fullhtml?archive=sTeX/Documentation&filepath=tutorial.en.xhtml

SIEX is a system for generating human-oriented documents in either PDF or HTML format, augmented with computer-actionable semantic information (conceptually) based on the OMDoc format and ontology.

In this part, we will give a broad but shallow introduction to SIEX, and what you can get out of it. Additionally, this serves as an introduction to the SIEX IDE, and we consequently assume that you have that one set up, as described in section 1.5.

Note that in PDFs, the specific highlighting of semantically annotated text is fully customizable (see chapter 9). In this document, we use this highlighting for notation components, this highlighting for symbol references, this highlighting for (local) variables and this highlighting for definienda; i.e. new concepts being introduced.

## Chapter 2 The Basics

This document itself uses \(\lessapprox\)TeX and serves as a direct example for the following. You can download its source files, the generated PDF files, and the generated HTML documents directly from within the IDE, by navigating to the SLEX tab in the menu on the left and finding sTeX/Documentation in the list of math archives and clicking the small "Install"-button next to it, see the screenshot on the left of Figure 2.

Once downloading is finished (this may take a while since dependencies are also downloaded), you can then browse the.tex-files in sTeX/Documentation directly from the math archives panel in the SLEX tab, as you can see in the right screenshot in Figure 2.

For example, you can now navigate to the file tutorial/intro.en to see the sources of this very chapter.

As a first example, consider the following document fragment from section 1.1:

\(\lessapprox\)TeX is a system for generating human-oriented documents in either PDF or HTML format, augmented with computer-actionable semantic information (conceptually) based on the OMDoc format and ontology.

If you were to look at the generated HTML from this fragment, you could hover over the highlighted words (\(\lessapprox\)TeX, PDF, HTML, OMDoc) and get a little popup with their definitions (Figure 3). Neat, huh?

Here, in the PDF, hovering will only show you a unique identifier (MMT-URI) for the word, and link to a definition on the web. Still useful, but not quite as neat, of course.

A plain LaTeX-version of the above document fragment, without any \(\lessapprox\)TeX markup, could look like this:

\(\blackbox\)

**Example 1**

Input:Figure 3: Definition on Hover

Figure 2: Installing Math Archives

File [sTeX/Documentation]tutorial/intro/introplain.en.tex

```
1\documentclass{article}
2\usepackage{stex-logo}
3\begin{document}
4
5\sTeX{}isasystemforgeneratinghuman-orienteddocuments
6ineither\textsf{PDF}or\textsf{HTML}format,augmented
7withcomputer-actionablesemanticinformation(conceptually)
8basedonthe\textsc{OMDoc}formatandontology.
9
10\end{document}
```

Output:

```
```
```

```
```
```

```
```
```

```
```
```

```
```
```

```
```
```

```

```

(Examples like the one above always show the file the source code is in, so if you have downloaded the sTeX/Documentation math archive you can toy around with it yourself)

If you save a file in the IDE (regardless of whether it has unsaved changes), a preview window will pop up, showing you the HTML generated from the.tex-file; see (Figure 4).

The \sTeX macro comes with the stex package as well, but if you only want to use the logo - e.g. to write eulogies about \(\sTeX\) in plan \(\sTeX\) papers, you can load the much smaller stex-logo package instead.

Figure 4: Previewing the document in the IDE

### Text symbols

The most central concept behind LaTeX is that of a _symbol_:

A symbol is a _named_ concept that can be defined, documented and referenced. Examples for symbols are mathematical constants, functions, theorems, statements, principles - anything that has a (somewhat) precise meaning and can be referenced by name can be a symbol.

Before we explain how we can declare new symbols and associate them with definitions, notations and all that, let's assume an ideal world in which others have done that job already for us - after all, LaTeX is all about _reuse_, and naturally, there are LaTeX symbols for all of the above already. Let's start with the one for LaTeX itself:

#### Using Modules & Search in the IDE

In the VS Code IDE, navigate to the LaTeX-tab on the left. In the search panel, select the "Symbols" radio button and search for "sTeX". The second search result should be what we're looking for (Figure 5).

Search results are grouped into _local_ and _remote_ results. Local ones are the ones you already have in your local MathHub directory; remote ones you can download directly from within the IDE.

You can click the preview button to see the generated HTML for the document - the resulting window that pops up also has an OMDoc tab you can select, which (among other things) shows you the semantic macros provided by the respective module: In this case, it tells us that there is a _text symbol_ named "sTeX" with semantic macro \stex in the module mod/systems/tex?sTeX that is in the \sTeX/ComputerScience/Software archive. It produces the presentation "SLEX" as we want (Figure 6).

If we want to use the LaTeX symbol in a document - which we have open in the IDE - we simply click on the use button, and the IDE will automatically insert the line \usemodule[sTeX/ComputerScience/Software]{mod/systems/tex?sTeX}, making all symbols in that module available to use - in particular, we can now use the \stex semantic macro instead of the plain, non-semantic \sTeX macro - that is, of course, after we include the \stex package first.

Analogously, we can also search for the PDF, HTML and OMDoc symbols, all of which are also text symbols and have the associated semantic macros \PDF, \HTML and \omdoc; the document should thus look like this:Figure 5: Search in the \(\mathfrak{SL}\)EX IDE


* highlight semantically annotated text in this color,
* show the MMT-URI of the corresponding symbol in a tooltip on hovering over the text,
* make the text link to the place the symbol is being defined in the current document (if it is), or, alternatively,
* make it link to an external resource, if one is known. In our case, they link to texmmt.mathhub.info/:sTeX, where the HTML for all the symbols we use in this document are hosted.

Note that in the IDE, the \usemodule-statement for OMDoc is underlined in blue (Figure 7) - VS Code is letting us know, that this \usemodule statement is _redundant_. That is because the \TEX module we imported earlier already imports the OMDoc module; as such we have all macros therein available already. If we look at the \TEX module in the VS Code preview window again, we can see that (Figure 8).

We can consequently safely delete the \usemodule again.

### 2.2 Symbol References

Let's continue with the next paragraph of section 1.1; for now unannotated:

**Example 3**

Input:

Figure 8: Includes in the OMDoc Preview

Figure 7: Redundant Imports

File [sTeX/Documentation]tutorial/intro/intro2plain.en.tex

1\documentclass{article}
2\usepackage{stex}
3\begin{document}
4
5At its core is the \sTeX{} package for \LaTeX, that allows for
6 semantically marking up document fragments; in particular
7 concepts, formulae and mathematical statements (such as
8 definitions, theorems and proofs). Running \texttt{pdflate}
9over \sTeX-annotated documents formats them into normal-looking
10textsf{PDF}.
11
12\end{document}

Output:

At its core is the SIEX package for LaTeX, that allows for semantically marking up document fragments; in particular concepts, formulae and mathematical statements (such as definitions, theorems and proofs). Running pdflate over SIEX-annotated documents formats them into normal-looking PDF.

We already know how to annotate "SIEX" and "PDF"; and if we use the search field in the IDE again, we can also find a text symbol for "LaTeX". But if we look at the documentation, we will note that _more_ is highlighted:

At its core is the SIEX package for LaTeX, that allows for semantically marking up document fragments; in particular concepts, formulae and mathematical statements (such as definitions, theorems and proofs). Running pdflate over SIEX-annotated documents formats them into normal-looking PDF.

The "package"-symbol can be found in the LaTeX module too, and searching for the keywords "formula" and "mathematics" will yield the symbols "well-formed formula" and "mathematics", but they are not _text symbols_ and "mathematics" and "package" do not even have a semantic macro - and the one for "well-formed formula" would not work outside of math mode.

Text symbols are special in that way - they are intended for symbols that have a specific formatting associated (such as LaTeX, OMDoc, or HTML, which we prefer to typeset as sans serif). For those settings, it makes sense to associate that formatting with a semantic macro that does the typesetting for us.

Symbols _without_ a text macro can be referenced with the \symname macro:

\symname{package} prints the _name_ of the "package"-symbol and annotates it accordingly, without any special formatting - in particular it is compatible with being in \emph, \textbf and similar macros. That takes care of _one_ of the missing annotations.

More generally, the \symref macro can be used to annotate arbitrary text with a symbol: \symref{mathematics}{mathematical} associates the text mathematical with the symbol "mathematics"; thus, we get "mathematical" and similarly "formulae".

\begin{tabular}{l l} \begin{tabular}{l l} \begin{tabular}{l l} \begin{tabular}{l l} \hline \hline \multicolumn{1}{c}{\begin{tabular}{l} \hline \hline \multicolumn{1}{c}{\begin{tabular}{l} \hline \hline \multicolumn{1}{c}{\begin{tabular}{l} \hline \hline \multicolumn{1}{c}{\begin{tabular}{l} \hline \hline \hline \multicolumn{1}{c}{\begin{tabular}{l} \hline \hline \hline \multicolumn{1}{c}{\begin{tabular}{l} \hline \hline \hline \multicolumn{1}{c}{\begin{tabular}{l} \hline \hline \hline \hline \multicolumn{1}{c}{\begin{tabular}{l} \hline \hline \hline \hline \multicolumn{1}{c}{\begin{tabular}{l} \hline \hline \hline \hline \multicolumn{1}{c}{
\begin{tabular}{l} \hline \hline \hline \hline \end{tabular} \\ \hline \hline \hline \hline \end{tabular} \\ \hline \hline \hline \end{tabular} \\ \hline \hline \end{tabular} \\ \hline \hline \end{tabular} \\ \hline \hline \end{tabular} \\ \hline \end{tabular} \\ \hline \end{tabular} \\ \hline \end{tabular}

The "package"-symbol can be found in the LaTeX module too, and searching for the keywords "formula" and "mathematics" will yield the symbols "well-formed formula" and "mathematics", but they are not _text symbols_ and "mathematics" and "package" do not even have a semantic macro - and the one for "well-formed formula" would not work outside of math mode.

Text symbols are special in that way - they are intended for symbols that have a specific formatting associated (such as LaTeX, OMDoc, or HTML, which we prefer to typeset as sans serif). For those settings, it makes sense to associate that formatting with a semantic macro that does the typesetting for us.

Symbols _without_ a text macro can be referenced with the \symname macro:

\symname{package} prints the _name_ of the "package"-symbol and annotates it accordingly, without any special formatting - in particular it is compatible with being in \emph, \textbf and similar macros. That takes care of _one_ of the missing annotations.

More generally, the \symref macro can be used to annotate arbitrary text with a symbol: \symref{mathematics}{mathematical} associates the text mathematical with the symbol "mathematics"; thus, we get "mathematical" and similarly "formulae".

\begin{tabular}{l l} \begin{tabular}{l l} \hline \hline \hline \multicolumn{1}{c}{\begin{tabular}{l} \hline \hline \hline \multicolumn{1}{c}{\begin{tabular}{l} \hline \hline \hline \multicolumn{1}{c}{\begin{tabular}{l} \hline \hline \hline \multicolumn{1}{c}{\begin{tabular}{l} \hline \hline \hline \multicolumn{1}{c}{\begin{tabular}{l} \hline \hline \hline \multicolumn{1}{c}{\begin{tabular}{l} \hline \hline \hline \multicolumn{1}{c}{\begin{tabular}{l} \hline \hline \hline \multicolumn{1}{c}{
\begin{tabular}{l} \hline \hline \hline \hline \end{tabular} \\ \hline \hline \hline \end{tabular} \\ \hline \hline \hline \end{tabular} \\ \hline \hline \end{tabular} \\ \hline \end{tabular} \\ \hline \end{tabular} \\ \hline \end{tabular} \\ \hline \end{tabular}
\end{table}
Table 1: The _name_ of the symbol,2. the name of its semantic macro, 3. or any suffix of its MMT-URI containing at least the module name. The second option is often short - and therefore convenient to write; for example, to achieve "formulae", we can also write \symref{wff}{formulae}, since \wff is the semantic macro for "well-formed formula". The third option allows for distinguishing between multiple symbols with the same name - the IDE can help in the latter case, by underlining ambiguous symbol references in yellow, and offering the Quick Fix functionality to let you select and autocomplete the specific symbol you want to reference.

Since \symname and \symref are a lot to type for something that should ideally be used as often as possible, the macros \sn and \sr exist as well and behave exactly the same way. We also provide some convenience abbreviations for \sn; namely \Sn (capitalizes the first letter of the symbol name), \sns (adds an "s" at the end, for the most common pluralization of a name), and \Sns (both).

Using all of the above, our annotated fragment now looks like this:

**Example 4**

Input:

File [sTeX/Documentation]tutorial/intro/intro2stex.en.tex

5 \usermodule[sTeX/ComputerScience/Software]{mod/systems/tex?sTeX}

6 \usermodule[sTeX/Logic/General]{mod/syntax?Formula}

7 \usermodule[sTeX/MathBase/General]{mod?Mathematics}

8 \usermodule[sTeX/ComputerScience/Software]{mod/formats?PDF}

9
10 At its core is the \stex \sn{package} for \later, that allows for semantically marking up document fragments; in particular

12 concepts, \sr{wff}{formulae} and \sr{mathematics}{mathematical}

13 statements (such as definitions, theorems and proofs). Running

14 \text{tpdflatex} over \stex-annotated documents formats them

15 into normal-looking \PDF.

Output:

At its core is the \STEX package for \ITEX, that allows for semantically marking up document fragments; in particular concepts, formulae and mathematical statements (such as definitions, theorems and proofs). Running pdflatex over \STEX-annotated documents formats them into normal-looking PDF.

There's only one problem: _the document does not compile_, with an error Undefined control sequence. The reason being that _some_ macro in the module Formula uses the \text macro. We can fix that by using the amsfonts package of course, but this points to a more general problem; namely that modules can make use of various LaTeX packages for typesetting symbols.

Good practice suggests putting those packages into a _prelude_ per math archive, which we can then import from anywhere, using the \libinput macro. For more on that, see section 5.3.

For now, suffice it to say that we can import all packages required for the module Formula from the math archive sTeX/Logic/General by adding the line 


...and open the file helloworld.tex with the content

```
\documentclass{stex} \libinput{preamble} \begin{document} %AfirstsTeXdocument \end{document}
```

You can now reference any newly created content in you new archive using for example \usemodule[my/archive]{...}.

Let's start with the "LaTeX" symbol. Rename the file helloworld.tex to something more meaningful, for example latex.en.tex - the.en will be picked up on by \TeX to signify that the fragment will be in _english_ (see subsection 7.1.1).

What we want to achieve in this file is the following:

```
\TeXis a document typesetting software developed by Donald Knuth, with a focus on mathematical formulae. It is based on a powerful and extensible macro expansion engine. \TeX is a (nowadays) default collection of TeX macros developed by Leslie Lamport. Among other things, LaTeX introduces environments, a distinction between preamble and document content, packages to bundle and distribute macro definitions, and document classes: special packages that govern the global layout of a document.
```

In particular, in the HTML the two paragraphs above should be shown when hovering over the symbols they define (as indicated by the magenta definiendum highlighting). So we need symbols and semantic macros, for: TeX, macro, LaTeX, environment, package and document class.

Symbol declarations are only allowed within modules:

``` \begin{document} \begin{smodule}{LaTeX} \end{table} \end{table}
Table 1: The IDE immediately picks up on this and displays the full MMT-URI of our new module over the \begin{smodule}{LaTeX} (Figure 10) –From this, we can glimpse that the namespace of the module is

[http://mathhub.info/my/archive/latex](http://mathhub.info/my/archive/latex). This implies, that to use the module somewhere else, we will have to type \usemodule[my/archive]{latex?LaTeX} - the latex-part pointing to the _file_ and LaTeX referring to the actual module.

If we rename the file to LaTeX.en.tex, we notice that the namespace changes to [http://mathhub.info/my/archive](http://mathhub.info/my/archive), allowing us to now use it with

\usemodule[my/archive]{LaTeX} directly. That's because the module name LaTeX and the file name LaTeX match now (see section 7.5, Figure 11).

Within the module, we can now declare new symbols using the \symdecl-macro. We start with those that are not text symbols:

\symdecl*{macro}

\symdecl*{environment}

\symdecl*{package}

\symdecl*{document class}

The * after the \symdecl indicates, that we do not want a semantic macro for the symbol - otherwise, it would generate one with the same name as the symbol itself and "pollute the macro space", so to speak.

The symbols TeX and LaTeX, however, have a definite way of being typeset associated with them, which can be produced using the standard \TeX and \LaTeX macros. So let's make them text symbols, using the \textsymdecl macro:

\textsymdecl{tex}{\TeX}

\textsymdecl{latex}{\LaTeX}

The first argument being the name of the generated macro (i.e. \tex and \latex) and the second one specifying the output to produce.

Figure 11: VS Code Code Lense

Figure 10: VS Code Code Lense

### 2.4 Documenting Symbols

We can now use the two new macros, \symname/\sn, \symref/\sr etc. to mark up the above two paragraphs. But the IDE also makes us aware of the symbols not yet being documented, via squiggly blue lines(Figure 12).

Among other things, this means that the system does not yet know what to show a reader when hovering over the symbol in the HTML. The IDE also recommends two ways to fix that: The sdefinition or sparagraph environments.

Ignoring the former for now, which is more useful for mathematical concepts, we can use the following to mark up the first paragraph:

\begin{sparagraph}[style=symdoc,for={tex,macro}] \tex is a document typesetting  software developed by Donald Knuth, with a focus on  mathematical formulae. It is based on a powerful  and extensible \sn{macro} expansion engine. \end{sparagraph}

In general, the sparagraph environment can be used to mark up arbitrary paragraphs semantically, but the style=symdoc option tells \TeX to use this paragraph as a documentation for the symbols provided in the for= option. And indeed, doing so makes the squiggly blue lines in the IDE under \textsymdecl{tex}{TeX} and \symdecl*{macro} disappear.

We just used the semantic macro \stex and the \sn macro to mark up the fragment - but we can do better. Both concepts are being _introduced_ in the above paragraph, and we can let \TeX know that that is the case:

Within an sparagraph environment with style=symdoc (or an sdefinition environment), we can mark up _definienda_, meaning the terms _being defined_, explicitly. Analogously to \symname and \symref, we have the macros \definiame and \definiendum for that purpose.

Note that the \tex macro induced by the text symbol above already marks up the "TeX" it produces, so wrapping it in another \definition would be redundant. However, every text symbol also generates a _second_ macro with the suffix name that generates a non-marked-up version of the same presentation. In other words, we get the macro \texname for free, that produces "TeX" (of course, we could just as well use the \TeX macro, but that one you probably know already).

Furthermore, every \definiendum or \definiame automatically adds the symbol being referenced to the internal for=list of the sparagraph environment, obviating the need to list it explicitly.

As such, we can produce a better markup like this:

\begin{sparagraph}[style=symdoc] \definitionand{tex}{texname} is a document typesetting

Figure 12: Undocumented Symbolssoftware developed by Donald Knuth, with a focus on mathematical formulae. It is based on a powerful and extensible \(\backslash\)definame{macro} expansion engine. \(\backslash\)end{sparagraph}

**Exercise**

In your archive my/archive, create additional files that produce the following outputs:

Mathematics.en.tex

To do **mathematics** is to be, at once, touched by fire and bound by reason. This is no contradiction. Logic forms a narrow channel through which intuition flows with vastly augmented force.

- Jordan Ellenberg

PDF.en.tex

**Portable Document Format** (PDF) is a document format that mixes text and graphics with a variety of content.

HTML.en.tex

The **HyperText Markup Language** (HTML) is a representation format for web-pages.

OMDoc.en.tex

OMDoc is a document format for representing mathematical documents with their flexiformal semantics.

such that the following file compiles and shows the above snippets on hover:

1 \documentclass{stex}

2 \libinput{preamble}

3 \begin{document}

4 \begin{smodule}{sTeX}

5 \usemodule{_OMDoc_}

6 \usemodule{_PDF_}

7 \usemodule{HTML}

8 \text{textsymdecl}{_{sTeX}}

9 \begin{sparagraph}{style=symdoc}

10 \definition{_{stex}}{\{_{\text{streamame}}\}} is a system for generating

11 documents in either \PDF or \HTML format, augmented with

12 computer-actionable semantic information (conceptually)

13 based on the \(\backslash\)OMDoc format and ontology.

14 \end{sparagraph}

15 \end{smodule}

16 \end{document}

STEX is a system for generating documents in either PDF or HTML format, augmented with computer-actionable semantic information (conceptually) based on the OMDoc format and ontology.

The preamble of every file should only be \documentclass{stex} \libinput{preamble} and the macros \OMDoc, \PDF, \HTML should produce \textsc{OMDoc}, \textsf{PDF} and \textsf{HTML}, respectively (but with semantic annotations of course). _Solution:_ Can be found in [sTeX/Documentation]source/tutorial/solution

### 2.5 Sectioning and Reusing Document Fragments

We know now how to import and reuse the symbols of some module (using \usemodule). What about the actual document _content_?

Assume we want to write a new article that includes all of the fragments in my/archive we made so far, in a file all.en.tex in the same math archive:

```
1\documentclass{article}
2\usepackage{stex}
3\libinput{preamble}
4\begin{document}
5\author{Me}
6\title{The \textttt{my/archive} Archive}
7\maketitle
8\tableofcontents
9...
10\end{document}
```

In there, we want sections as follows:

```
-1Preliminaries (Mathematics) -1.1DocumentFormats (PDF) (HTML) (OMDoc) -2\TeXandFriends (LaTeX) (sTeX)
```

We could of course do the following:

```
\section{Preliminaries} \input{Mathematics.en} \subsection{DocumentFormats} \input{PDF.en} \input{HTML.en} \input{OMDoc.en} \section{TeX andFriends} \input{LaTeX.en} \input{sTeX.en}
```

...but this approach has two drawbacks:

Firstly, we need to manually keep track of the section levels, by explicitly writing \section, \subsection etc. This is fine as long as we are just interested in this particular article. But what if we want to _reuse_ the article's content in another document at some point? The section levels might be entirely different then - e.g. we might want the "Preliminaries" section to be a subsection instead.

Secondly, the \input macro considers the file name/path provided to be either _absolute_ or relative to the _current_tex_file being compiled_ - which means that the \input{Mathematics.en} only works for files in the same directory as Mathematics.en.tex.

In short: using \section, \chapter etc. explicitly, and \input to reuse fragments, breaks reusability.

Instead of using \section and \subsection, \slEx therefore provides the sfragment environment.

\begin{sfragment}{Foo}...\end{sfragment} inserts a sectioning header depending on the current section level and availability. These are: \part, \chapter, \section, \subsection, \subsubsection, \paragraph and \subparagraph. This allows us to do the following instead:

\begin{sfragment}{Preliminaries}

\input{Mathematics.en}

\begin{sfragment}{Document Formats}

\input{PDF.en}

\input{HTML.en}

\input{OMDoc.en}

\end{sfragment}

\end{sfragment}

\begin{sfragment}{{YeX and Friends}

\input{LaTeX.en}

\input{SrTeX.en}

\end{sfragment}

The only problem remaining now is that if we do this, \slEx will insert a \part for the first sfragment. If we want the "top-level" sectioning level to be \section instead, we can insert a \sectionlevel{section} in the preamble.

As a more reuse-friendly replacement of \input, \slEx provides the \inputref macro. Using that has two advantages: Firstly, its argument is relative to some (optionally provided, or the current) math archive and is thus independent of the specific location of the file relative to the currently being compiled.tex-file. Secondly, when converting to HTML, it will _not_ "copy" the referenced file's content in its entirety (as \input would), but instead dynamically insert the already existent (if so) HTML of the referenced file, avoiding content duplication and having to process the file all over again.

In general \inputref[some/archive]{file/path} inputs the file file/path.tex in the archive some/archive. As the \input-ed files in the example above are in the same archive anyway, we can simply substitute the \inputs by \inputrefs and call it a day.

Finally, we can make two more minor changes:

1. The _title_ of our document is only supposed to be there, if we compile the document directly - if we were to \inputref our file into a "driver file" all.en.tex, the title and the table of contents should be omitted. We can achieve this using the \ifinputref conditional: by wrapping the header in an \ifinputref \else...\fi, it will only be processed if the file is _not_ being loaded using \inputref. \ifinputref is a "classic" \slEx conditional and is treated as such in both PDF and HTML compilation. A smarter macro to use is \IfInputref, which takes two arguments for the _true_ and _false_ cases, respectively.

Additionally, when compiling to HTML, _both_ arguments to \IfInputref will be processed, and the backend will decide which of the two to present when serving a document.
2. The table of contents should also be omitted in HTML mode. To achieve that, we can use the \ifstexhtml conditional, which is _true_ if the document is being compiled to HTML, and _false_ if compiled to PDF.

In summary, we can modify our document to do the following:

 \IfInputref{  \author{Me}  \title{The \textttt(my/archive} Archive}  \maketitle  \ifstexhtml\else\tableofcontents\fi  \} The final all.en.tex can be found in [sTeX/Documentation]tutorial/solution/all.en.tex.

### 2.6 Building and Exporting HTML

So far we know how to write \flex documents, (we assume) how to build PDF files from them (via pdflatex of course), and on saving documents the IDE will preview the generated HTML. But if we do that with our new all.en.tex, we get presented with Figure 13 Where did all of our fragments go?

Well, they don't exist yet as HTML. The HTML Preview window in the IDE is really just that: A _preview_. But when using \inputref, it has to find the HTML of the \inputrefed fragment _somewhere_. Meaning: we have to compile all of the fragments we used to HTML first. Individually, we can compile the currently open file in VS Code using the button in Figure 14.

This will do the following:

1. Run pdflatex over the file three times.
2. Store the resulting.pdf in [archive]/export/pdf/<filepath>.pdf.

Figure 13: Missing Fragments in the HTML Preview

3. Convert the file to HTML and store it in [archive]/xhtml/<filepath>.xhtml.
4. Extract all the semantics and store them as OMDoc in [archive]/content/...., [archive]/narration/.... and [archive]/relational/....
5. Construct a search index in [archive]/export/lucene/....

Doing all of this for every individual file _in hindsight_ would of course be a huge hassle. We can therefore just compile the full archive, folders in an archive, or whole _groups_ of archives via right-clicking an element in the Math Archives viewer in the SLEX tab (Figure 15).

Once that's done, saving all.en.tex again yields the correct HTML in the preview window.

At this point, it should be noted that you can't actually just open the HTML files exported to [archive]/xhtml in your browser and get all of the expected functionality - that shouldn't be too surprising. Features like the fancy pop-up windows require a semantically informed backend infrastructure, in the form of the Mmt system. However, Mmt_can_ dump a standalone version for you. Let's do that now:

With our all.en.tex file open and everything built as above, click the Export Standalone HTML button in the IDE (see Figure 16).

In the dialog box that opens now, select an **empty** directory and Mmt will dump a standalone version of our all.en.tex document there. You will still not be able to

Figure 14: The Build PDF/XHTML/OMDoc Button

Figure 15: Building Archives in the IDE

open it in the browser directly, because most browser forbid javascript modules on the file:// protocol, but opening the file via http will yield the desired result, and you can now upload the directory's content to wherever you might want to use it.

If you want to test this, a quick and easy way to do so is to use VS Code: You can install the Live Server extension, open the directory and click the Go Live button on the lower right of the window, which will start a small web-server in the selected directory and open its index.html in the browser for you.

Figure 16: Exporting HTML in the IDE

## Chapter 3 Mathematical Concepts

So far, we have seen how to declare and reference symbols generate semantic macros for text symbols, collect them in modules and document them properly.

But where LaTeX really shines is when it comes to mathematics and related subject areas: semantic macros are significantly more useful when used for generating symbolic notations in math mode, and by associating symbols with (flexi-)formal semantics, LaTeX can even _check_ that your content is (to some degree) formally correct, or at least well-formed.

Alos LaTeX provides specialized functionality for mathematical statements: the text fragments marked as Definition, Theorem, Proof that are iconic to mathematical documents.

The example snippets in this chapter can be found in the math archive sTeX/MathTutorial. If you downloaded the sTeX/Documentation archive in the LaTeX IDE, you already have that archive. If not, you can download it from within the IDE, as described in chapter 2.

### 3.1 Simple Symbol Declarations

We will start with symbols and semantic macros for mathematical concepts and objects and their contribution to mathematical formulae.

#### Semantic Macros and Notations

Let us start with a very fundamental concept; namely equality. As you should by now know, declaring a new symbol requires a module, so let's open a new one and use \symdecl:

\begin{smodule}{Equality}

\symdecl{equal}

\end{smodule}

As mentioned in section 2.3, the starred variant \symdecl* does not create a semantic macro, so presumably, the variant without a * _does_. And indeed, we now have a macro \equal, which however will produce errors if we try to use it. That's because we haven't told LaTeX what to do with it yet.

A **semantic macro** is a LaTeX-macro that allows for referencing a symbol itself, or - in the case of e.g. a function - the _application_ of a symbol to (one or multiple) _arguments_; primarily by invoking a symbol's notation in _math mode_.

The command \symdecl{macroname} declares a new symbol with name macroname and a semantic macro \macroname. In the case where we want the name and the semantic macro to be distinct, the command \symdecl{macroname}[name=some name] declares the name of the symbol to be some name instead.

The starred variant \symdecl*{name} declares the concept with the given name, but does not generate a semantic macro.

So let's provide equality with a notation. As a first step, we should let SLEX know that "equal" takes two arguments. We might also want to shorten the semantic macro to e.g. \eq, without changing the name. Hence:

\symdecl{eq}[name=equal,args=2]

Next, we add an infix notation with the \notation macro:

\notation{eq}{#1 = #2}

That seems like a lot to write, so for the very common case where we want to declare a symbol with a semantic macro and a notation all at once, the \symdef macro does all three by combining the optional and mandatory argument of \symdecl and \notation:

\symdef{eq}[name=equal,args=2]{#1 = #2}

and indeed, we can now use the \eq macro in math mode to invoke our new notation: $|eq{a}{b}$ now yields \(a=b\) - notably without any highlighting (and hover interaction in the HTML) though. Since our semantic macro takes _arguments_, which should be differently highlighted, we need to let our notation know which parts of the notation are highlightable components.

We can do so with the \comp and \maincomp macros:

The \comp-macro marks components to be highlighted in a notation for a symbol taking (one or more) arguments.

This is necessary because it is (nearly) impossible for LaTeX to figure out, which parts of a notation to highlight and which not on its own - in particular, the highlighting should stop for the _arguments_ of a semantic macro.

Additionally, the \maincomp macro can be used to mark (at most) one notation component to represent the _primary_ component of the notation.

Notations that do not take arguments, as well as operator notations, are automatically wrapped in \maincomp.

In our case, this applies only to the "=", symbol, so:

\symdef{eq}[name=equal,args=2]{#1 \mathrel{\maincomp{=}} #2}

You may be wondering about the role of the \mathrel macro in the example above: TeX determines spacing/kerning in math mode by assigning a _class_ to every character. Both individual characters and whole subexpressions can be assigned one of these classes using dedicated macros. These are:Having done so, we can now type $|eq{a}{b}$ to get \(a=b\). Thanks to using \maincomp, we now also have an operator notation, which we can invoke using $|eq!$, yielding =.

What if we want to add more notations? Say we want to be able to invoke equality to get the variant notation \(a\equiv b\) ()without changing the intended meaning). If we want to be able to choose one of several notations, we should give the notation an _identifier_.

Let's again modify our earlier notation by adding the identifier eq to the optional arguments of \symdef, like so:

\symdef{eq}[name=equal,args=2,eq]{#1 \mathrel{\maincomp{=}} #2}

We can now invoke the specific notation provided here by writing $|eq[eq]{a}{b}$ to the same effect. But we can also add more notations using the \notation macro:

\notation{eq}[equiv]{#1 \mathrel{\maincomp{\equiv}} #2}

which we can now invoke with $|eq[equiv]{a}{b}$, yielding \(a\equiv b\).

By default, the _first_ notation provided for a given symbol is considered the _default_ notation, which is invoked if the semantic macro is used without an optional argument - hence, $|eq{a}{b}$ still yields \(a=b\).

If we use the starred variant of the \notation macro, the notation is set as the new default. Hence, had we done

\notation*{eq}[equiv]{#1 \mathrel{\maincomp{\equiv}}} #2}

then $|eq{a}{b}$ would now yield \(a\equiv b\).

Any already existing notation can be set as default using the \setnotation macro; e.g. instead of using \notation*, we could also do

\notation{eq}[equiv]{#1 \mathrel{\maincomp{\equiv}}} #2}

\section{setnotation{eq}{equiv}

**Exercise**

Implement the symbol "equal" as above in a new module "Equality" and add a documentation such that hovering over the symbol in the HTML yields the following snippet:

Two objects \(a,b\) are considered \(\mathsf{equal}\) (written \(a=b\) or \(a\equiv b\)), if there is no property that distinguishes them.

_Solution:_ Can be found in [sTeX/MathTutorial]/mod/Equality1.en.tex

#### 3.1.2 Types and Variables

You might have noticed - after you save the file - that the expressions $|eq{a}{b}$ and $|eq[equiv]{a}{b}$ are underlined in yellow in the IDE and have a warning attached to them (Figure 17).

If we click on the Invalid Unit link in the error message, we get a somewhat cryptic stacktrace-like window (Figure 18).

The reason being, that Mmt actually tries to formally verify _everything we write using semantic macros!_ It does so, by attempting to infer the _type_ of an expression - success implies that the expression is in fact well-typed.

If the former paragraph is difficult to comprehend for you, don't worry - you'll likely pick up on things as we go along. For now, sufice it to say that we can assign "_types_" to symbols, and the Mmt system is smart enough to use those to check that what we're writing actually "makes sense"; for example, \(a+b\) makes perfect sense if \(+\) is addition and \(a\) and \(b\) are numbers, or elements of a vector space, but not if \(a\) and \(b\) are, say, triangles.

Figure 17: Type Checking Warning

Figure 18: Type Checking Proof TreeIn order to _formally verify_ a mathematical statement, we have to rely on a set of _rules_ that determine what is or isn't a valid statement. There are many systems of such rules with very different flavours, called **(logical) foundations.**

The most commonly used foundation in (informal) mathematics is _set theory_, in particular _ZFC_; a set of axioms in (usually) _first-order logic_. However, in _computer proof assistants_ and similar systems, _type theories_ like _higher-order logic_ or the _calculus of (inductive) constructions_ are more popular, because they lend themselves better to computer implementations.

In as far as possible, we prefer to remain "foundationally agnostic", or **foundation independent**: Every foundation has advantages and disadvantages, and which one is appropriate often depends on the particular setting one is working in.

Nevertheless, certain "meta-principles" have proven themselves to be extremely effective in representing and checking mathematical content in software, and while we do not fix a particular foundation or specific checking rules, we will make use of those principles in general. These include e.g. the _Curry-Howard Correspondance_, or _Judgments-as-Types paradigm_, and _Higher-Order Abstract Syntax_.

Full formal verification of document content is an extremely lofty goal, and hardly realistic if you're not willing to write your content in pretty specific ways, and informed by a decent amount of background knowledge in formal logic. Moreover, formally verifying content in LaTeX is an ongoing research project, so we will not go into the specifics in detail here.

While full formal verification is out of reach for now, annotating adequate types can strike a useful balance between the effort required and the benefit of automated meaning checking afforded by them. In this sense LaTeX is pragmatically similar to programming languages where adding types can raise the quality and correctness assurance in programs.

Types are particularly useful for _variables_:

A **variable** represents a _generic_ or _unspecified_ object.

Variables can be declared using the \vardef-macro, whose syntax is analogous to \symdef.

Note that variables are local to the current TeX-group (e.g. environment).

Let's leave our equality-module aside for now and turn our attention to something simpler: natural numbers. Consider the following module:

**Example 5**

Input:

\begin{smodule}{Nat} \symdef{Nat}[name=naturalnumbers]{\mathbbN} \begin{sparagraph}[style=symdoc]  The \defname{Nat}$\defnotation{\Nat}$ are the numbers $0,1,2,...$ \end{sparagraph} \symdef{plus}[name=addition,args=2]{#1\mathbin{\maincomp{+}}#2} \begin{sparagraph}[style=symdoc] \Defname{addition}$\defnotation{\plus{a}{b}}$ \refers to the process of adding two \n{Nat}. \end{sparagraph} \end{smodule}

Output:

```
ThenaturalnumbersN are the numbers 0,1,2,... Addition\(a+b\) refers to the process of adding two natural numbers.
```

(like \defname and \definiendum, the \defnotation macro is only allowed in documenting environments like sparagraph[style=symdoc] or sdefinition, and highlights the notation components marked with \comp or \maincomp the same way as \defname and \definiendum do.)

Note, that as the \Nat semantic macro does not take any arguments, we do not need to wrap the notation in a \comp or \maincomp.

Note also, that the \plus{a}{b} is again underlined in the IDE with an Invalid Unit warning.

The above fragment uses two variables \(a\) and \(b\). In fact, Mmt will consider them variables even though they are not marked up as such - but since they are not marked up, we are missing out on useful functionality.

Let's change that by adding two variable definitions1:

Footnote 1: Technically, this is called a _variable reservation_, for those in the know.

```
\begin{sparagraph}[style=symdoc] \vardef{\va}[name=a]{a}\vardef{\vb}[name=b]{b} \Defname{addition}$\defnotation{\plus{\va}{\vb}}$ \refers to the process of adding two \n{Nat}. \end{sparagraph}
```

Output:

```
Addition\(a+b\) refers to the process of adding two natural numbers.
```

Okay, so now \(a\) and \(b\) are gray, but besides that, we haven't achieved much yet.

Let's change that by giving the variables the type \(\mathbb{N}\):

**Example 7**

Input:

```
\begin{sparagraph}[style=symdoc] \vardef{va}[name=a,type=|Nat]{a}\vardef{vb}{name=b,type=|Nat]{b} \Definance{addition}$\defnotation{\plus{\vu}{\vvb}}$ \refers to the process of adding two \sn{Nat}. \end{sparagraph}
```

Output:

```
```

**Addition**\(a+b\) refers to the process of adding two natural numbers.

_Now_ if we hover over the \(a\) and \(b\) (in the HTML), it will show us that their type is \(\mathbb{N}\)!

We can of course also assign types to symbols. In the IDE, find the symbol _"function space"_ with semantic macro \funspace (in [sTeX/MathBase/Functions]{mod?Function}). The OMDoc preview window shows you how to use this symbol (Figure 19).

This tells us that if we write \funspace{a_1,...,a_n}{b} (depending on which notation we use), we will get \(a_{1}\times...\times a_{n}\to b\).

We want addition to have type \(\mathbb{N}\times\mathbb{N}\to\mathbb{N}\), hence we do: \(\verb|symdef|plus|[name=addition,args=2,\verb|type=|funspace|Nat,|Nat]{#1\mathbin{\maincomp{+}}#2}
```

So far (and when using the use button in the IDE), we have been using the \usermodule macro to import content. \usermodule is allowed anywhere and imports the referenced module content local to the current TeX group.

Now that we use imported symbols in types (and since we are _in_ a module), we need to make sure that the imported modules are also (transitively) _exported_, since our new symbols now _depend_ on the imported module.

Figure 19: Syntax PreviewFor that we use the \importmodule macro within the module; i.e. the file should now look something like this:

\begin{tabular}{l l} begin{smodule}{Nat} \\ \importmodule[sTeX/MathBase/Functions]{mod?Function} \\ \... \\ \end{tabular}

Note that the HTML is aware of this now (after you save): _Clicking_ on any occurence of addition now yields Figure 20.

However, the squiggly yellow Invalid Unit warnings are still there - that's because everything we did with types so far still depends on our natural numbers symbol, which does not have a type yet.

By virtue of using [sTeX/MathBase/Functions]{mod?Function}, we also imported [sTeX/MathBase/Sets]{mod?Set}, which gives us the _"collection"_ symbol. Let's use this as a type for the natural numbers:

\symdef{Nat}[name=natural numbers,type=\collection]{mathbb N}

Now if we save the file, all the squiggly lines are gone. Moreover, if you look at the OMDoc tab in the preview window, you can find Figure 21. The **Document Elements**

Figure 21: Inferred Type

Figure 20: On-Click Popup in the HTML

block collects all semantically annotated expressions in a module or document; including variables and the $\plus{\vab}{\vb}$. Here, it tells us that it has checked the expression \(a+b\) (in the context of \(a:\mathbb{N}\) and \(b:\mathbb{N}\)), and inferred that it has type \(\mathbb{N}\).

Here's what just happened:

1. The Mmt system realized, that $\plus{\vab}{\vb}$ is the symbol "addition" applied to the two arguments \(a\) and \(b\).
2. It knows, that "addition" has type \(\mathbb{N}\times\mathbb{N}\to\mathbb{N}^{2}\).
3. It knows, that this means that if the two arguments \(a\) and \(b\) both have type \(\mathbb{N}\), then the full expression has type \(\mathbb{N}\).

Here's something you can now try: If we _remove_ the types from the variables \(a\) and \(b\) again, the warnings are _still_ gone. We lose the type information on hover, but Mmt still doesn't complain, because it now realizes that since \(a\) and \(b\) have no explicit types given, it should infer them. And by the same chain of reasoning as above, it can infer that since they are being used as arguments for addition, they need to have type \(\mathbb{N}\).

#### Flexary Macros and Argument Modes

Here is one thing you might wonder: Writing $\plus{a}{b}$ is one thing, but what if we want to produce \(a+b+c+d+e\)? Do we really need to write $\plus{a}{\plus{b}{\plus{c}{\ldots}}}$?

Of course not. We can declare the symbol such that the semantic macro \plus expects a (comma-separated) _sequence_ of arguments instead of two "normal" arguments.

The optional args-argument of \symdecl expects a string of characters indicating the semantic macro's argument modes. There are four such modes:

i a simple argument,

a a- (_left or right) associative_ - sequence argument, represented as a single TeX-argument {a,b,...},

b A binding argument that expects a variable that is bound by the symbol in its application, and

B A binding sequence argument of arbitrarily many bound variables by the symbol ({x,y,z,...}).

If args is given as a number \(n\) instead, the semantic macro takes \(n\) arguments of mode i.

**Example 8**:
* For \plus{a,b,c} yielding \(a+b+c\), we do \symdecl{plus}[args=a],
* for \inset{a,b,c}{A} yielding \(a,b,c\in A\), we do \symdecl{inset}[args=ai],
* in \add{i}{1}{n}{f(i)} yielding \(\sum_{i=1}^{n}f(i)\), the variable \(i\) is bound in the expression, we hence do \symdecl{add}[args=biii],



ments, so if we have a type of "truth values", it makes sense to model "equal" as a function taking two arguments and returning that type. So we do type=\funspace{......?

Here's the idea with respect to _implicit arguments_. Let's first declare a new variable of type "collection":

\vardef{\A}[name=a,type=\collection]{A}

We now assign the type \(A\times A\to\Prop\) to equal:

\symdef{eq}[name=equal,args=2,eq,type=\funspace{\A\_V\A\}\{\prop\}]{\#1\mathellationrel\maincomp{=}}#2}

(The symbol "proposition" with semantic macro\prop comes with \(\$\TeX\) directly; we say that it is part of the \(\$\TeX\).)

Now our type has a free variable \(A\). For Mmt, this now means that equal actually takes _one more argument_, but one whose value is uniquely determined from the other arguments. Indeed, if you consider equal to take three arguments (the first one being some \(A\) of type collection), then the _next_ two arguments _enforce_ that the first argument has to be the type of the other two.

In other words: \(A\) is now an implicit argument that Mmt is tasked with inferring whenever we use equal, and that we never explicitly provide in \(\$\TeX\).

Indeed, if we use our module Nat from before, and apply \eq to a variable of type \(\N\), Mmt does not complain:

\usemodule{mod?\_Nat}

\vardef{\n}[name=n,type=\Mat]{n}

\$\eq{\n}{m}$

And if we inspect the OMDoc tab in the HTML preview, we can see exactly what Mmt did (Figure 22).

1. (by the \(\cdot\)\(\ldots\)) that Mmt considers \(A\) an implicit argument in the type of equal,

Figure 22: Implicit Arguments

2. that the _inferred_ type of \(n=m\) is Prop,
3. that Mmt inferred the implicit argument of equal in \(n=m\) to be \(\mathbb{N}\) (by the \(\underbrace{\ldots}_{\mathbb{N}}\)), and
4. that it was enough to give \(\verb|vn|\) the explicit type \(\mathbb{N}\) - Mmt also inferred that hence \(m\) also has to have type \(\mathbb{N}\)

#### Finishing Equality

You might wonder if - as with addition - we can make "equal" take a sequence argument as well. Naturally, we can:

```
1\symdef{eq}[name=equal,args=a,eq,
2type=\funspace{vA,vA}{prop}
3]{\argsep{\#1}{mathrel{\maincomp=}}}
4\notation{eq}[equiv]{\argsep{\#1}{mathrel{\maincomp\equiv}}}
```

and as before, we now get Invalid Unit warnings. Unlike before, however, we can not just fix this with adding assoc=bin. As mentioned, bin instructs Mmt to "fold" the symbol over the arguments, so when doing {eq{a,b,c}, Mmt would turn this into equal(a,equal(b,c)), i.e. the claim that _"a" is equal to "b = c"_ - but that's not what \(a=b=c\) means. What we mean by \(a=b=c\) is really "\(a=b\)_and_\(b=c\)".

For that, we can use assoc=conj - however, that requires that some symbol that can be used for _conjunction_ (i.e. "and") is in the current scope.

If we search for conjunction in the IDE, we should find the module

```
[sTex/Logic/General]{mod/syntax?Conjunction}.
```

Using that, we can now write the following:

```
\usemodule{mod?Nat} \usemodule{sTex/Logic/General}{mod/syntax?Conjunction} \vardef{vn}{name=n,type=\_Nat}{n} \$eq{\vn,m,p}$}
```

Upon saving, Mmt does not complain; and if we inspect the OMDoc tab in the HTML window again, we now notice that Mmt correctly resolved this as in Figure 23.

#### Variable Sequences

There is a special kind of variable in sTeX for when we want to use _sequences_ of variables.

We can use the \varseq macro to declare a new sequence variable; in the simplest case that looks something like the following:

```
\varseq{seqn}[name=n,type=\_Nat]{1,\ellipses,k}{\maincomp{n}_{\#1}}
```

We have just declared a new variable sequence of type \(\mathbb{N}\), that ranges over indices \(1,\ldots,k\), with notation \(n_{i}\) for some specific index \(i\).

If we now do \seqn{i}, we get \(n_{i}\), and if we do \seqn{1}, we get \(n_{1},\ldots,n_{k}\).

We can also do multi-dimensional sequences, e.g.

```
\varseq{seqm}[name=m,type=\_Nat,args=2] {{1}{1},\ellipses,{\ell}{k}} {\maincomp{m}_{\#1}^{\#2}}
```Now \seqm{i}{j} produces \(m_{i}^{j}\), and \seqm! produces \(m_{1}^{1},\ldots,m_{\ell}^{k}\).

Of course, we can manually change the way \seqm! is typeset by providing an explicit operator notation using op=; e.g. if we do

\varseq{seqm}[name=n,type=\Mat,op={(n_i)_{i=1}^k}]

{1,\ellipses,k}{(maincomp{n}_{#1}}

then \seqm! produces \((n_{i})_{i=1}^{k}\).

So far so nice, but sequence variables get especially useful in combination with sequence arguments: Consider for example the \plus semantic macro for addition. This expects one sequence argument, or alternatively, a _sequence variable_: \_plus{\seqm} now produces \(n_{1}+\ldots+n_{k}\), and \seq{\seqm} now produces \(m_{1}^{1}=\ldots=m_{\ell}^{k}\).

TODO4
Footnote 4: TODO: seqmap

### 3.2 Statements

Now that we have equality, natural numbers, addition and multiplication at our disposal, let's implement some _statements_. Both addition and multiplication are, for example, _associative_ and _commutative_.

We could state these properties directly for the two operations, but we can also first define _associativity_ and _commutativity_ in general, and then assert them specifically for addition and multiplication.

#### Definitions

Let's define what it means to be _associative_. This means, of course, declaring a new symbol. Note that we don't need a semantic macro for associativity, since there is no notation to attach to it. We will also for now ignore its type. Note however, that associativity is still a property of (binary) operations, so it still makes sense to have the symbol take an _argument_; namely the operation it applies to.

Figure 23: Conjunction of Equalities

We will also finally provide an actual (more or less) formal _definition_ for the symbol, so where we used the sparagraph environment with style=symdoc before, we will now use the sedfinition environment, which also gives us \definance, \definiendum, \defnotation and all that.

A first variant of a corresponding module could look like this:

**Example 9**

Input:

```
File[sTeX/MathTutorial]props/Associative1.en.tex
4\begin{smodule}{Associative}
5\importmodule{mod?Equality}
6
7\symdecl*{associative}[args=1]
8\begin{sdefinition}{for=associative}
9\vardef{\vA}[name=A,type={collection}]{A}
10\vardef{vop}[name=op,type={funnspace{\vA},\vA}\vA,args=a,assoc=bin]
11\{argsep{\#1}{\mathbin{\mathincomp{\virc}}}}
12\%
13Abinaryoperation${\fun{vop1}{\vA},\vA}\vA$iscalled
14\def{\#element{associative},if
15\$eq{\vop{\{\vop1,\{vop2,\{b,c\}}\}}}
17\vop{a,\{\vop2,\{b,c\}}}
18\$forall$inset{a,b,c}\vA$.
19\end{sdefinition}
20\end{smodule}
```

Output:

**Definition 3.2.1**.: A binary operation \(\circ:A\times A\to A\) is called associative, if \((a\circ b)\circ c=a\circ(b\circ c)\) for all \(a,b,c\in A\).

Note, that the semantic macros \fun and \inset come from
[sTeX/MathBase/Functions]mod?Function and [sTeX/MathBase/Sets]mod?Set, respectively. Also note, that the variable declaration for \vop makes use of all the fun features we already discussed for addition.

Note that the above is more than good enough, if you merely want to produce nice-looking, "wikified" HTML and PDF documents. The rest of this subsection will cover how to add more flexiformal semantics to the above.

If this seems laborious and/or difficult, keep in mind that this is to some degree experimental still, and you are not forced to go overboard with semantic annotations!

But if you aim to create a "library of symbols" for mathematical concepts, then all of the possibilities that we discuss here will add value for the community. Generally, the higher the ratio of readers to authors the more any investment in semantization will pay off.

#### Semantic Macros in Text Mode

The first thing we can do to further improve this document is marking up the "for all" in the definition - after all, there naturally is a symbol for the universal quantifier, which can be found in [sTeX/Logic/General]mod/syntax?UniversalQuantifier and has the semantic macro \forall (as to not conflict with the TeX primitive macro \forall).

The naive approach would be to replace the "for all" by e.g. \sr{for all}{for all}. That would (correctly) associate and highlight the text fragment with the symbol "universal quantifier", _but_ we are not just referencing the symbol here - we are actually using it, by _applying_ it to the variables \(a,b,c\) and the expression \((a\circ b)\circ c=a\circ(b\circ c)\).

In _math mode_, we can just use the semantic macro \forall - that will take two arguments (of modes B and i) and produce the corresponding notation, so that

 $\forall{\inset{a,b,c}{\vA}}{ \eq{\vop{(\vop{a,b}),c},\vop{a,(\vop{b,c})}}} }

will produce \(\forall a,b,c\in A.(a\circ b)\circ c=a\circ(b\circ c)\).

In _text mode_, however, we don't have a specific notation - instead, the specific "notation" is whatever sentence we want to mark up semantically. In text mode, semantic macros therefore behave differently:

1. They take _precisely_ one argument, regardless of how many arguments the macro would take in math mode or (equivalently) the args property of the symbol.
2. _Within_ that argument, we can use \comp to highlight arbitrary text fragments, and
3. we can use the \arg macro to mark up the _actual_ arguments that the symbol is supposed to be applied to. \arg takes as optional argument the index of the argument that is being marked up; if not they are used consecutively. The starred variant \arg* produces no output.

So we could now do

 \forall{\comp{For all} $\arg{\inset{a,b,c}{\vA}}$, we have $\arg{ \eq{\vop{(\vop{a,b}),c},\vop{a,(\vop{b,c})}}}$ }

which produces "For all \(a,b,c\in A\), we have \((a\circ b)\circ c=a\circ(b\circ c)\)".

In our case though, we want to "switch the arguments around" - first comes the equation, then the variables to be bound. Hence:

 $\arg[2]{ \eq{\vop{(\vop{a,b}),c},\vop{a,(\vop{b,c})}} }

 \comp{for all} $\arg[1]{\inset{a,b,c}{\vA}}$

which produces "\(a\circ b)\circ c=a\circ(b\circ c)\) for all \(a,b,c\in A\)".

#### Definientia

Now we have a fully semantically annotated expression in the definition for "associative". Can we let Mmt know, that this expression really is _the_ definition of the symbol?

Yes, we can. All we need to do is wrap the sentence in a \definiens macro (plural: _definientia_; like the word _"definiendum"_ refers to "the term being defined", _"definiens"_ refers to "the thing the term is being defined _as_").

The \definiens macro is only allowed within the sdefinition environment, and requires that the environment lists the symbol that gets the definiens attached explicitly in its for= argument. It is possible to attach definientia to multiple symbols within an sdefinition environment, in which case the symbol needs to be provided as an optional argument, e.g. we could do \definiens[associative]{...}. Since "associative" is the only symbol being defined in our definition, we can omit that argument.

Alternatively, as with types we can attach definientia to a \symdecl directly using the optional argument def=....

At this point, you might justifiably wonder, why we even still need to declare associative with \symdecl* before we define it. And indeed, we don't - the sdefinition environment takes the same optional arguments as the \symdecl macro, and if we explicitly provide a name= (or a macro=), it will generate a symbol for us. We can hence get rid of the \symdecl* and instead do:

```
1\begin{sdefinition}[name=associative,args=1]
2...
3\end{sdefinition}
```

One more problem remains: We stated that associative is to take one argument - but we haven't told \fTeX what it is yet. In our case, the argument is represented by the variable \vop. In fact, chances are that arguments to symbols in types or definientia are almost always represented by some variable.

We can use one of two ways to a variable as being an argument:

1. If the variable (e.g. \vop with name op) was already declared prior to the sdefinition environment, we can use the \varbind macro in the environment; e.g. by adding \varbind{op}.
2. We can move (or copy) the \vardef for the variable into the environment and add bind to its optional arguments.

In total, our fully annotated definition now looks like this:

```
1Example10Input:


Combining this with what we just learned, we can now say that addition is associative by doing:

\symuse{associative}{$}arg{\}plus!}$\compt{isassociative}}

In fact, we would do the exact same thing every time we want to say that _some_ operator is associative, so it makes sense to introduce a macro for this. In fact, such a macro is easy to define using standard LaTeX methods. This is where \STEXexport becomes very handy:

In a module, we can put arbitrary LaTeX code in an \STEXexport, and this code will be executed every time the module is imported via \usemodule or \importmodule. This is especially useful for macro definitions, and this way modules can almost act like LaTeX packages!

So we can define a new macro \isassociative that applies "associative" to an arbitrary operation and produces the semantically marked-up text "#1 is associative", and wrap that macro definition in an \STEXexport, and whenever we use the Associative module, we also get the \isassociative macro:

\STEXexport{

\def\isassociative#1{

\symuse{associative}{\arg{#1} ~is ~\comp{associative}}}

}

And now, we can do e.g. \isassociative{$}plus!} to produce "+ is associative".

For technical reasons, \STEXexport processes its content in the expl3 category code scheme - what this means is that all spaces are ignored entirely, and the characters _ and : are valid characters in macro names.

In practice, this means you will have to use the - character for spaces, and if you want to use a subscript _, you should use the macro \c_math_subscript_token instead.

**Exercise**

Analogously to all the above, implement a module for _commutativity_; i.e the property of a binary operation that \(a\circ b=b\circ a\) for all \(a,b\). Make the module export a macro \iscommutative analogously to \isassociative.

_Solution:_ Can be found in [sTeX/MathTutorial]props/Commutative.en.tex

TODO5
Footnote 5: TODO: intent?

#### Assertions

Having defined associativity and commutativity, we can now assert that both properties hold for addition and multiplication.

For _assertions_ (i.e. theorems, lemmata, axioms, claims,...), \STEX provides the sassertion environment.

In the simplest case, that can look like the following:

\begin{sassertion}

\isassociative{\Sn{plus}}

\end{sassertion}

which yields

Addition is associative

Do we want this to be typeset as a **Theorem**? For that we just add a [style=theorem] to the sassertion environment, provided we have a customization for that - (see chapter 9). We can also load the **texthm** package, which uses the amsthm package to provide common typesettings for the types: theorem, observation, corollary, lemma, axiom and remark.

So far, this is not too useful - after all, we could have just as well used e.g. the amsthm package and gone straight for the non-sfhex variant

```
\begin{theorem} \issorsociative{\Sn{plus}} \end{verbatimend{verbatim}
```

But as with sdefinition, we can immediately add a corresponding symbol in the sassertion environment, and have it be documented directly by the environment:

```
\begin{sassertion}[style=theorem,name=additionisassociative] \issorsociative{\Sn{plus}} \end{verbatim}
```

And now, if we do \sn{addition is associative}, we get addition is associative with a corresponding hover pop-up (in the HTML).

Of course, the usefulness of this grows with more elaborate assertions. For very short assertions such as the above, we might not even want to typeset them in such a space hungry manner.

For that purpose, we provide the \inlineass macro (and analogously: \inlinedef for sdefinition), which takes the same optional arguments as the environment. So we could also do:

```
\inlineass[name=additionisassociative]{\issorsociative{\Sn{plus}}}
```

So far, Mmt is blissfully unaware of the semantic contents of our assertions. We can easily remedy that by wrapping the expression representing the assertion in a \conclusion macro, analogously to the definiens macro in sdefinitions:

```
\inlineass[name=additionisassociative]{\nconsociative{\Sn{plus}}} \end{verbatim}
```

We can now see the statement in the OMDoc tab of the HTML preview (Figure 25).

Not exactly pretty - the OMDoc tab uses notations to render content, and we did not provide any for associative.

Notice the \- symbol after the name of the assertion? As an aside for those who are curious:

Figure 25: Assertion Statement in OMDoc

The judgments as types paradigm represents the validity of proposition via a designated _type of proofs_: For any proposition \(P\), we introduce a collection \(\vdash P\) of _proofs_ of \(P\).

To say that the proposition _holds_ is then equivalent to positing that _some_ element \(p:\vdash P\) exists - in which case _proofs_ become typed objects in their own right.

Let's consider a more interesting statement now. How about the induction axiom?

\begin{sassertion}{style=axiom,name=induction axiom}

Let ${varphi(n)$ a property on \sn{Nat}. If \begin{enumerate} \item ${varphi(0)$ and \item if ${varphi(m)$ holds for some $m$, then ${varphi(\plus{m,1})$ also holds, \end{enumerate}} then ${varphi(n)$ holds for all ${inset{n}}{Nat}$. \end{enumerate}}

**Axiom 3.2.3**.: _Let \(\varphi(n)\) a property on natural numbers. If_

1. \(\varphi(0)\) _and_
2. _if_ \(\varphi(m)\) _holds for some_ \(m\)_, then_ \(\varphi(m+1)\) _also holds,_

_then_ \(\varphi(n)\) _holds for all_ \(n\in\mathbb{N}\)_._

**Exercise**

Annotate the above by:

1. Variables with appropriate notations for \(\varphi\), \(m\) and \(n\), and
2. marking up the second premise ("if \(\varphi(m)\) holds for some...") in text mode as the formula \(\forall m.\varphi(m)\Rightarrow\varphi(m+1)\) using the semantic macros \forall (which we saw earlier already) and \imply (implication) from [sTeX/Logic/General]mod/syntax?Implication. The text fragments that should be highlighted are "if" and "then".
3. marking up the conclusion ("\(\varphi(n)\) holds for all \(n\in\mathbb{N}\)") in text mode as the formula \(\forall n.\varphi(n)\). The text fragment that should be highlighted is "for all".

_Solution:_ Can be found in [sTeX/MathTutorial]mod/NatTheorems.en.tex

So how can we teach Mmt the semantics of this statement? Here's what we can do:

1. As with the simpler assertions (and hence the name), the _conclusion_ of the assertion can be marked up with \conclusion.
2. As with sdefinition, we can mark variables as _bound_ (using either bind in the \vardef or \varbind). _If_ a symbol that can act as a universal quantifier is in scope, variables marked as bound are abstracted away using that symbol.
3. Similarly to \conclusion, _premises_ can be marked up as such using the \premise macro. If a symbol is in scope that can act as an implication, that will be used to connect the premise(s) to the conclusion.

Hence, if we mark the variable \(\varphi\) as bound and use \(\backslash\)premise and \(\backslash\)conclusion (see [sTeX/MathTutorial]mod/NatTheorems.en.tex), we can inspect the OMDoc tab in the HTML preview again and see that Mmt has now constructed the proposition (Figure 26).

#### Proofs

A common concept in mathematics is that of a mathematical structure - a _tuple_ of interdependent components. For example: A _monoid_ is a structure \(\langle M,\circ,e\rangle\) such that certain axioms hold; where \(M\) is a set, \(\circ\) is a binary operation, and \(e\in M\).

From a representational perspective, this is particularly interesting: \(M\), \(\circ\) and \(e\) in the above are not symbols in the same way that the previous symbols we considered were - they don't represent definite objects. Instead, they are _components_ of some other object, namely a monoid; where a _particular_ monoid could either be a fixed object (such as \(\langle\mathbb{Z},+,0\rangle\)) or an _indefinite_ monoid; i.e. a variable. We call the components of a mathematical structure **fields**.

In this section, we will discuss how to declare and use mathematical structures in STeX, build them up modularly, and connect them among each other to avoid duplication.

We will do so by considering _lattices_ both algebraically and order-theoretically, and identify the two perspectives.

#### Declaring and Using Structures

The simplest kinds of structures are _magmas_ and _(directed) graphs_, so we might as well start there:

**Definition 3.3.1**.: A **magma** is a structure \(\langle U,\circ\rangle\), where \(U\) is a collection and \(\circ\) a binary operation \(U\times U\to U\).

The obvious start is to create a new module Magma. Within this module, we import the Functions module so we can later assign a type to the operation. We can then use the mathstructure environment, that creates a new symbol "magma":

Figure 26: The Induction Axiom in OMDoc

<begin{smodule}{Magma} <importmodule[sTeX/MathBase/Functions]{mod?Function} <begin{mathstructure}{magma}... <end{mathstructure} <end{smodule}

mathstructure behaves very similarly as smodule - within the environment, we can declare new symbols, notations and all that.

So within the mathstructure, we can add symbols for the two fields \(U\) and \(\circ\):

<symdef{univ}[name=universe,type={collection}{U} <symdef{op}[name=operation,args=a,assoc=bin, type={funspace{univ,univ}univ}]{univ

!{\argsep{#1}{mathbin{\maincomp{\circ}}}}

Once we close the environment (with \end{mathstructure}), the symbols are "gone". However, we now have a new symbol "magma" with semantic macro \magma. It's usage is somewhat more complicated than "normal" semantic macros, but one thing we _can_ do with it now is $\magma1$, which will produce \(\langle U,\circ\rangle\).

Notably however, the \magma macro is already available _within_ the mathstructure environment as well.

This allows us to provide an sdefinition using the semantic macros declared in the structure:

**Example 11**: Input:

File [sTeX/MathTutorial]algebra/Magma.en.tex
7 <begin{mathstructure}{magma}
8 <symdef{univ}[name=universe,type={collection}{U}
9 <symdef{op}[name=operation,args=a,assoc=bin, type={funspace{univ,univ}univ}
11 <argsep{#1}{\mathbin{\maincomp{\circ}}}
12 <begin{sdefinition}{for={magma,univ,op}}
14 <A <definance{magma} is a <=<symdef{mathstruct}{structure} $\magma1$, where $\minv$ is a <=<symdef{collection} and $\op!$
16 <binary operation $\funspace{univ,univ}univ$.
17 <end{sdefinition}
18 <end{mathstructure}

Output:

**Definition 3.3.2**.: A magma is a structure \(\langle U,\circ\rangle\), where \(U\) is a collection and \(\circ\) a binary operation \(U\times U\to U\).

#### Instantiating Structures

More importantly however, we can now declare a variable magma, using the optional return= argument. For example, we can now do

<vardef{vM}[name=M;return=\magma]{M}

and we get the semantic macro \VM with which we can do the following:


sequence \vMs is the index, when doing \vMs{i}... the #1 in the return-statement will be replaced by i.

Also, note that if we want to produce \(M_{i}\) - i.e. the magma at index \(i\) in the sequence, we can do \vMs{i}!.

Think of the! as a "stop sign" - if the expression up to the! has an associated presentation, the! tells \fEX to "stop eating arguments" and present whatever it has until now.

#### Extending Structures and Axioms

It is extremely common to "build up" structures in a hierarchical manner by adding new fields or axioms: A _semigroup_ is an associative magma. A _band_ is an idempotent semigroup. A _monoid_ is a semigroup with a unit. A _partial order_ is an antisymmetric preorder.

We alluded to the fact earlier, that the mathstructure environment behaves like an smodule - that is literally true: Every mathstructure foo in a module FooMod is in fact also a module?FooMod/foo-module. We can therefore easily extend structures using \importmodule{...?FooMod/foo-module} - but extending structures is so common, and using \importmodule triing, that there is a shortcut: the extstructure environment. It takes as second argument a comma-separated list of structure names. That allows us to easily define semigroups:

**Example 12**

Input:

File [sTeX/MathTutorial]algebra/Semigroup.en.tex

```
8\begin{extstructure}{semigroup}{magma}
9\begin{sdefinition}
10A\definemme{semigroup}is a\sn{magma}${semigroup!$,
11where\inlinesas[name=associativeaxiom]{
12\conclusion{\issassociative{$|op!$}}.
13}
14\end{sdefinition}
15\end{extstructure}
```

Output:

**Definition 3.3.3**.: A semigroup is a magma \(\langle U,\circ\rangle\), where \(\circ\) is associative.

Note our usage of \inlineas to generate a new symbol for the associative axiom.

If we look at the OMDoc tab in the HTML preview window, we can see the output in Figure 27.

So Mmt has decided that our statement is an _axiom_.

#### Conservative Extensions

For structures, there is a _critical_ distinction between _defined_ and _undefined_ symbols; and analogously between _theorems_ and _axioms_.

Remember that structures are more like _templates_ that are _instantiated_ by particular objects. An _undefined_ field in a structure, in that sense, is like an _obligation_: If something is supposed to be a semigroup, it _has to_ have a universe, an operation and the operation needs to satisfy the associative axiom.

_Defined_ fields on the other hand have a _definiens_ on the basis of the remaining fields - they don't need to be explicitly provided for something to instantiate the structure; if all the _undefined_ fields are provided, the _defined_ ones we get _"for free"_.

The same holds for _theorems_: If a statement is _provable_ from the axioms, then we don't need to explicitly prove it to hold for some particular instance - we have a proof already, provided the axioms hold.

One consequence of this is: Extending a structure only by _defined_ fields does not actually (conceptually) introduce a _new_ structure - every instance of the old one _should_ also be an instance of the new one. The new fields are basically just "syntactic sugar".

There is a name for extending a structure only by defined fields (or theorems): A _conservative extension_.

Slex provides the extstructure* environment for that purpose. Unlike extstructure, it does _not_ take a name (technically, Slex generates one internally). Instead, conceptually extstructure* modifies the extended structure directly, rather than generating a new structure. The caveat however is, that every symbol introduced in an extstructure* **must** be defined.

Consider the following conservative extension:

**Example 13**

Input:

Figure 27: Axioms in OMDoc

```
File [sTeX/MathTutorial]algebra/MagnaSquare.en.tex
```
7\begin{extstructure*}{magma}
8\begin{sdefinition}[macro=sg,args=1]
9\notation{sg}[op=cdot=2]{{#1}~{\comp2}}
10\vardef{va}[name=a,type=|univ,bind]{a}
11Let$inset{\vaf}{univ}$. We define
12$\defnotation{\sg{\vaf}}:=\{\definiens{\op{\vaf,\vaf}}$.
13\end{lstlisting}
14\end{lstlisting}

Output:

```
**Definition 3.3.4**.: Let \(a\in U\). We define \(a^{2}:=a\circ a\).

Via \definiens, the new symbol sq is now _defined_ (note the macro= argument, taht generates a semantic macro as well). Whenever we import the containing module, we now have an additional field sq in (any extension of) magma - e.g., the following is now valid:
``` \usermodule[sTeX/MathTutorial]{algebra?MagmaSquare} \vardef{vsg}[name=S,return=\semigroup]{S} \vsg{sq}{a}$...producing \(a^{2}\).

#### Nesting Structures and \this

A prehaps not too surprising, but a notable aspect of structures is that fields themselves can be instances. This is important for example for implementing _vector spaces_, but can also be used to bundle things that are not normally thought of as structures, such as objects with certain defining properties.

Take as an example, the notion of a (magma) homomorphism:

**Definition 3.3.5**.: Let \(M_{1}=\langle U_{1},\circ_{1}\rangle\) and \(M_{2}=\langle U_{2},\circ_{2}\rangle\) magmas. A **magma homomorphism** is a function \(F:U_{1}\to U_{2}\) such that \(F(a\circ_{1}b)=F(a)\circ_{2}F(b)\) for all \(a,b\in U_{1}\).

So a homomorphism is a function with certain properties. And structures can be used to "bundle" the function itself with both the magmas on whose universes the function operates, as well as the _axiom_ that _makes_ it a homomorphism. After all, considered as a mere function, \(F:U_{1}\to U_{2}\) contains no information about the operation with respect to which it is homomorphic.

The first thing to note is that we can provide mathstructure with an optional argument for a _name_ distict from the name of its semantic macro. We then add two fields that return magmas. So far, so unexciting:

```
\begin{mathstructure}{magmahom}{magmahomomorphism} \symdef{dom}{name=domain,return={\magma[comp={#1}_{1}]}}{M_{1} \symdef{cod}{name=codomain,return={\magma[comp={#1}_{2}]}}{M_{2}} \symdef{f}[type=\funspace{\}dom{univ}}{\}{\{\}cod{univ}},args=1]{???}
```


Note how - as one would expect - we can treat \(\backslash\)vh{dom} and \(\backslash\)vh{cod} like any other instance of magma.

Note that some of the outputs in the above table are probably not quite what we want. Determining the precise typesetting of an expression involving _nested paths_ of fields is difficult, to say the least (e.g., what exactly should \(\backslash\)this refer to in a deeply nested sequence of fields?).

Using instances within structures is still very useful; at the very least when defining structures. When subsequently _using_ structures, however, accessing fields of fields (of fields (of...)) of an instance should be avoided.

Luckily, there is rarely a need for doing so - in practice, those fields we might want to access in such a way, we usually also want to provide specific notations and talk about independently of the "containing" instance, such that introducing a new variable (or symbol), and assigning the corresponding field to that variable, makes considerably more sense. And subsequently using the variable is easier than concatenating {...}, too.

### 3.4 Complex Inheritance and Theory Morphisms

We are starting to approach seriously experimental territory.

While the theory behind all the following is relatively well understood, and their implementation in Mmt is mature, the same can not be said out the implementation in STeX.

There are still kinks to be ironed out, but feel free to experiment.

We now have all the tools available to progress towards something more interesting. Here is a list of documents with respective modules and symbols we will build on in the following:

[sTeX/MathTutorial]props/Idempotent.en.tex

**Definition 3.4.1**.: Let \(e\in A\) and \(\circ:A\times A\to A\). \(e\) is called **idempotent** with respect to \(\circ\), if \(e\circ e=e\).

**Definition 3.4.2**.: The operation \(\circ:A\times A\to A\) is called **idempotent**, if every element \(a\in A\) is idempotent with respect to \(\circ\).

**Definition 3.4.3**.: Let \(\odot:B\times A\to A\) and \(\oplus:A\times A\to A\). We say \(\odot\)**distributes over \(\oplus\)**, if \(b\odot\left(a_{1}\oplus a_{2}\right)=\left(b\odot a_{1}\right)\oplus\left(b\odot a _{2}\right)\) for all \(a_{1},a_{2}\in A\) and \(b\in B\).

**Definition 3.4.4**.: Let \(\odot:A\times B\to A\) and \(\oplus:A\times B\to B\). We say \(\odot\)**absorbs**\(\oplus\), if \(a_{1}\odot\left(a_{1}\oplus b\right)=a_{1}\) for all \(a_{1}\in A\) and \(b\in B\).

**Definition 3.4.5**.: A **band** is an idempotent semigroup.

**Definition 3.4.6**.: A **semilattice** is a commutative band.

**Definition 3.4.7**.: A binary relation \(R\) on \(A\) is called **reflexive**, if \(R(a,a)\) for all \(a\in A\).

**Definition 3.4.8**.: A binary relation \(R\) on \(A\) is called **symmetric**, if \(R(a,b)\) implies \(R(b,a)\) for all \(a,b\in A\).

**Definition 3.4.9**.: A binary relation \(R\) on \(A\) is called **transitive**, if \(R(a,b)\) and \(R(b,c)\) implies \(R(a,c)\) for all \(a,b,c\in A\).

**Definition 3.4.10**.: A binary relation \(R\) on \(A\) is called **antisymmetric**, if \(R(a,b)\) and \(R(b,a)\) implies \(a=b\) for all \(a,b\in A\).

**[sTeX/MathTutorial]**props/Antisymmetric.en.tex**

**Definition 3.4.11**.: A **directed graph** is a structure \(\langle U,R\rangle\), where \(U\) is a collection and \(R\) a binary relation on \(U\).

**Definition 3.4.12**.: An **(undirected) graph** is a directed graph \(\langle U,R\rangle\), where \(R\) is symmetric.

**Definition 3.4.13**.: A structure \(\langle U,\leq\rangle\) is called a **preorder** (or **quasiorder**, or **preordered set**; in short **proset**), if \(\leq\) is reflexive and transitive.

**Definition 3.4.14**.: A preorder \(\langle U,\leq\rangle\) is called a **partial order** (or **poset**), if \(\leq\) is antisymmetric.

**Definition 3.4.15**.: Let \(\langle U,\leq\rangle\) a poset. An element \(a\in U\) is called an **infimum** or **greatest lower bound** of \(x_{1}\) and \(x_{2}\), if \(a\leq x_{1}\), \(a\leq x_{2}\), and for any \(x\) with \(x\leq x_{1}\) and \(x\leq x_{2}\), we have \(x\leq a\).

**Definition 3.4.16**.: Let \(\langle U,\leq\rangle\) a poset. An element \(a\in U\) is called a **supremum** or **least upper bound** of \(x_{1}\) and \(x_{2}\), if \(x_{1}\leq a\), \(x_{2}\leq a\), and for any \(x\) with \(x_{1}\leq x\) and \(x_{2}\leq x\), we have \(a\leq x\).

**Definition 3.4.17**.: A poset \(\langle U,\leq\rangle\) is called a **meet semilattice** if for every two elements \(a,b\) the infimum \(a\wedge b\) exists.

**Definition 3.4.18**.: A poset \(\langle U,\leq\rangle\) is called a **join semilattice** if for every two elements \(a,b\) the supremum \(a\lor b\) exists.

**Definition 3.4.19**.: An **(order) semilattice** is a meet and join semilattice.

**Exercise**

Try to implement all of the above yourself!

#### Glueing Structures Together

We now want to progress towards lattices, i.e. the following:

**Definition 3.4.20**.: A lattice is a structure \(\langle U,\wedge,\vee\rangle\) such that \(\langle U,\wedge\rangle\) and \(\langle U,\vee\rangle\)are semilattices, and \ absorbs \ and vice versa; i.e. \(a\vee(a\wedge b)=a\) and \(a\wedge(a\lor b)=a\). The operations \ and \(\vee\) are called **meet** and **join**, respectively.

So we make a new module, open an extstructure environment and... realize two problems:

1. We can't just extend semilattice: We need _two_ copies of semilattice that share a universe, and importing semilattice twice is of course redundant.
2. We also want to _rename_ the operations of the two semilattices to be subsequently called join and meet.

What we need is a way to _inherit_ from semilattice while a) _modifying_ the symbols therein, and b) not be idempotent - i.e. two imports from the same structure or module should not be identified. We can do that with the \copymod macro, which takes three arguments:

1. A _name_ for the copy,
2. the structure or module to copy, and
3. a comma-separated list of renamings and redefinitions of the symbol. \(\langle\)_symbol\(\rangle\)=\(\langle\)_def\(\rangle\)_redefines \(\langle\)_symbol\(\rangle\)_, \(\langle\)_symbol\(\rangle\)@\(\langle\)_newname\(\rangle\)_renames it, \(\langle\)_symbol\(\rangle\)=\(\langle\)_def\(\rangle\)@\(\langle\)_newname\(\rangle\)_ (or \(\langle\)_symbol\(\rangle\)@\(\langle\)_newname\(\rangle\)=\(\langle\)_def\(\rangle\)_) does both.

In our case, we want two copies of semilattice, which we will call meetsl and joinsl. In the first copy, we only want to rename op to meet. In the second, we want to rename op to join, and _also_ redefine the universe to be the one from meetsl:

\copymod{meetsl}{semilattice}{ op @ meet }{\copymod{joinsl}{semilattice}{ univ = \univ, op @ join }

You might have already noticed some problem with that - which of the two universes does \univ refer to now? (They are _defined_ as equal, but LaTeX does not know that!) Or which of the two commutative axioms does "commutative axiom" refer to now? Everything is ambiguous now!

Not really - if you have wondered why the \copymod takes a _name_ as argument: The name is prefixed to every symbol name. Hence, the universe in joinsl is now called joinsl/universe, and the one in meetsl is called meetsl/universe. Furthermore, \copymod by default generates no semantic macros for any of the imported symbols - except for those renamed with @. In fact, what the @ syntax actually does, is to generated a semantic macro by that name. If we want to change the _name_ (that is shown when using \symname et al), we add that new name in square brackets. Hence, what we really want to do is:

\copymod{meetsl}{semilattice}{ univ @ univ, op @ [meet]meet } \copymod{joinsl}{semilattice}{ univ = \univ, op @ [join]joinThis now gives us two copies of semilattice, generates semantic macros \univ for meetsl/universe, \meet for meetsl/op and \join for joinsl/op, and renames meetsl/op to meet and joinsl/op to join.

That allows us to then add the absorption axioms, an \(\mathtt{sdefinition}\) for lattice and subsequently $\lattice!$ produces \(\langle U,\wedge,\vee\rangle\), with all axioms inherited (see [sTeX/MathTutorial]algebra/Lattice.en.tex).

#### Realizations

A very common situation we find in connection with mathematical structures is that "every _this_ is a _that_" (or the concrete case "_this_ is a _that_").

With what we did so far, we are in this situation regarding the algebraic definition of semilattices and the order-theoretic one (exemplary meet semilattice).

In \(\mathtt{Mmt}\) parlance, this corresponds to a total (implicit) theory morphism from "that" to "this".

In \(\mathtt{STeX}\) words, we want to inherit from "that" by assigning all the symbols in "that" to concrete terms. In our case:

[sTeX/MathTutorial]algebra/SemiLatticeOrder.en.tex

**Definition 3.4.21**.: Let \(\langle U,\circ\rangle\) a semilattice. We let \(a\leq b\) iff \(a\circ b=a\).

**Theorem 3.4.22**.: \(\langle U,\leq\rangle\) _is a meet semilattice._

Proof.: We need to prove the following

reflexivity \(a\leq a\): We need to show \(a\circ a=a\). Follows from the idempotent axiom.

antisymmetry \(a\leq b\) and \(b\leq a\) implies \(a=b\): Assume \(a\circ b=a\) and \(b\circ a=b=a\circ b\) (by the commutative axiom). Hence, \(a=b\)

transitivity If \(a\leq b\) and \(b\leq c\), then \(a\leq c\). : Assume \(a\circ b=a\) and \(b\circ c=b\) Then \(a\circ c=(a\circ b)\circ c=a\circ(b\circ c)=a\circ b=a\). Hence, \(a\leq c\).

\(a\circ b\) is the infimum of \(\{a,b\}\): By definition (and the commutative axiom), \(a\circ b\leq a\) and \(a\circ b\leq b\). We need to show, that if \(x\leq a\) and \(x\leq b\), then \(x\leq a\circ b\). Assume \(x\circ a=x\) and \(x\circ b=x\). Then \(x\circ(a\circ b)=(x\circ a)\circ b=x\circ b=x\). Hence \(x\leq a\circ b\)

So to be precise, we want to provide _definientia_ for all undefined symbols in meet semilattice (i.e. the relation and meet) and _proofs_ for all _axioms_ (reflexive axiom, anti-symmetric axiom, transitive axiom, and infimum axiom), and by so obtain the fact that every semilattice is a meet semilattice.

For that purpose, we have the \realize macro. It behaves like \copymod, but does not take a name, and additionally requires that all undefined fields get assigned. So we could do the following:

[style=offset,frametitle=Example 15,leftmargin=10pt]

Input:File [sTeX/MathTutorial]algebra/SemiLatticeOrder1.en.tex
8}begin{extstructure*}{semilattice}
9{realize{meets}}
10univ=univ,
11meet=top!,
12rel@[order]order=unap{a,b}{eq{\op{a,b},a}},
13reflexiveaxiom=trivial,
14transitiveaxiom=trivial,
15antisymmetricaxiom=trivial,
16infimumaxiom=trivial
17}
18vend{extstructure*}
19
20}vardef{mysl}{return={semilattice}{$}
21$}mysl{order}{a,b}{quad\mysl}{univ,op,order}$

Output:

\(a\leq_{S}b\)\(\langle U_{S},\circ_{S},\leq_{S}\rangle\)

As we can see, we can now access the field order, which is renamed from relation in meet semilattice and also has the desired definiens in Mmt. But of course this approach is very "declarative": We do all the assigning in one macro, rather than narratively as what they _should_ be: definitions and proofs.

If we want to achieve the more narrative version at the beginning of the subsection, we can use the realization environment instead. It behaves like the \realize macro, but allows us to do the assignments and renamings individually somewhere in the body of the environment, interleaved with arbitrary text. Additionally, within the environment, all SIFX features that introduce _definientia_ (like the \definiens macro) induce assignments instead.

To declaratively rename or assign fields, we can then use the \assign and \renamedecl macros instead. That allows us to do the following instead:

\begin{realization}{meets} \assign{univ}{\univ} \assign{meet}{\op{} \renamedecl}{rel}[order]{order} \(\ldots\)

...and then use text to do the remaining assignments. For example, we can use the \definition environment to assign rel to the desired definiens:

\userstructure{meets} \begin{sdefinition}{for=order} \verbind{va,vb}  Let$}semilattice!{univ,op}$a\sn{semilattice}.  Welet$}{rel{va,vb}$ \iff$}definiens{eq{\op{\va,vb},\vva}}$. \verbind{sdefinition}

And now SIFX will use the \definiens to assign \(a,b\mapsto a\circ b=a\) to the relation of meet semilattice.

Analogously, we can use the sproof and subproof environments to produce "definientia" (i.e. proofs) for the axioms (see [sTeX/MathTutorial]algebra/SemiLatticeOrder.en.tex)

## Chapter 4 Extensions for Education

The last two chapters have shown generic markup and semantization facilities in SSIFEX. As said before, investments in semantic markup pay off, iff the impact of a document is high, e.g. if there are many more readers than authors or if the semantic services afforded by the semantic markup can help reduce the help readers need to understand the material.

Educational documents constitute one category of high-impact documents which are supported by the SSIFEX ecosystem, we will cover them here.

### 4.1 Slides and Course Notes

todo6
Footnote 6: TODO: notesslides.sty

### 4.2 Problems and Exercises

todo7

Footnote 7: TODO: problem.sty

Footnote 8: TODO: hwexam.sty

## Part II User Manual

_The dynamic HTML version of this part can be found at_

[https://stexmmt.mathhub.info/](https://stexmmt.mathhub.info/):

sfeX/fullhtml?archive=sfeX/Documentation&filepath=manual.xhtml

## Chapter 5 Basics

### 5.1 Package and Class Options

* debug=_(prefixes)_: (see Developer Manual)
* lang=_(languages)_: If set, \(\$\mathrm{\SIEVX}\) will load the \(\mathsf{babel}\) package with the provided languages. Supported languages (currently) are: 

* mathhub=_(path)_: Uses the provided file path as MathHub directory (see section 5.2).
* usesms/writesms: If writesms is set, content loaded from external math archives (i.e. modules) is persisted in the file \jobname.sms. If usesms is set, the content of the.sms-file is loaded, obviating the need to reprocess the original files. The options are not mutually exclusive, but care should be taken if dependencies have changed between builds. This offers two advantages: 1. If a document has many (transitive) dependencies, usesms should significantly speed up the build process, and 2. setting usesms allows for distributing the.sms-file to make the document _standalone_, allowing for compilation without needing imported/used modules to be present.

The options debug, mathhub, usesms and writesms can also be set by the environment variables STEX_DEBUG, MATHHUB, STEX_USESMS and STEX_WRITESMS. In fact, the MATHHUB environment variable is the recommended way to set the MathHub directory. This is the only option where the _package option_ overrides the environment variable.

The environment variables for USE/WRITESMS are particularly useful, in that they allow for convenient compilation workflows. For example, the Build PDF/XHTML/OMDocbutton in the IDE does the following:

STEX_WRITESMS=true pdflatex <job>.tex
[bibtex|biber] <job>

STEX_USESMS=true pdflatex <job>.tex

Guaranteeing (in the first run) that all dependencies are loaded from their respective sources and persisted, and in the two subsequent runs read from the generated.sms file, (likely) speeding ub the subsequent runs significantly.

### 5.2 Math Archives and the MathHub Directory

STEX uses math archives to organize document content modularly, without a user having to specify absolute paths, which would differ between users and machines.

All STEX archives need to exist in the local MathHub-directory. STEX knows where this folder is via one of five means:

1. If the STEX package is loaded with the option mathhub=/path/to/mathhub, then STEX will consider /path/to/mathhub as the local MathHub directory.
2. If the mathhub package option is _not_ set, but the macro \mathhub exists when the STEX-package is loaded, then this macro is assumed to point to the local MathHub directory; i.e. \def\mathhub(/path/to/mathhub\usepackage\(\{\)stex\(\}\) will set the MathHub directory as path/to/mathhub.
3. Otherwise, STEX will attempt to retrieve the system variable MATHHUB, assuming it will point to the local MathHub directory. Since this variant needs setting up only _once_ and is machine-specific (rather than defined in tex code), it is compatible with collaborating and sharing tex content, and hence recommended.
4. If that too fails, STEX will look for a file -/.stex/mathhub.path. If this file exists, STEX will assume that it contains the path to the local MathHub-directory. This method is recommended on systems where it is difficult to set environment variables, and is used by the IDE setup.
5. Finally, if all else fails, STEX considers -/MathHub to be the MathHub directory.

The STEX IDE allows you to directly download math archives from gl.mathhub.info - currently available archives there are:

* a group of semi-experimental documents showcasing STEX3.3 features,
* a vast collection of multilingual modules of concepts in mathematics and computer science. The SMGloM predates STEX3 and is thus largely "underannotated" with respect to (formal) semantics,
* a vast collection of lecture slides and notes in computer science for courses held by Michael Kohlhase. They largely make use of SMGloM modules.

#### The Structure of Math Archives

An archive group/name is stored in the directory <MathHub>/group/name; e.g. assuming your local MathHub-directory is set as /user/foo/MathHub, then in order for the sTeX/Documentation archive to be found by the STEX system, it needs to be in /user/foo/MathHub/sTeX/Documentation.

Each such archive needs two subdirectories:

* this is where all your tex files go.
* a directory containing a single file MANIFEST.MF, the content of which we will consider shortly.

An additional lib-directory is optional, and is discussed in section 5.3.

#### MANIFEST.MF-Files

The MANIFEST.MF in the META-INF directory consists of key-value-pairs, informing STEX (and associated software, e.g. MMT) of various properties of an archive. For example, the MANIFEST.MF of the sTeX/Documentation archive looks like this:

id: sTeX/Documentation

ns: [http://mathhub.info/sTeX/Documentation](http://mathhub.info/sTeX/Documentation)

narration-base: [http://mathhub.info/sTeX/Documentation](http://mathhub.info/sTeX/Documentation)

format: stex

title: The sTeX Documentation

teaser: The full Documentation for the sTeX system

url-base: [https://stexmmt.mathhub.info/:sTeX](https://stexmmt.mathhub.info/:sTeX)

dependencies:sTeX/ComputerScience/Software,sTeX/MathTutorial

ignore: */code/*|*/tikz/*|*/tutorial/solution/*

Many of these are in fact ignored by STEX, but some are important:

id: The name of the archive, including its group (e.g. sTeX/Document). This is used by the MMT system in favor of the directory, but TeX's limited access to the file system enforces the directory structure.

source-base: or

ns: The namespace from which all symbol and module MMT-URIs in this archive are formed.

narration-base: The namespace from which all document MMT-URI in this repository are formed. It can safely match the ns-field.

url-base: A URL that is formed as a basis for _external references_. and hyperlinks. An MMT (or comparable system) instance should run there and host (STEX-generated) HTML.

dependencies: All archives that this archive depends on. STEX ignores this field, but MMT can pick up on them to resolve dependencies, e.g. when downloading archives in the IDE, which will also download all dependencies.

ignore: A regular expression of.tex files in the source directory that should be ignored; e.g. they will not be compiled when building a whole directory or archive in the IDE.


Then the preamble.tex files can take care of loading the generally required packages, setting presentation customizations etc. (per archive or archive group or both), and a postamble.tex can e.g. print the bibliography, index etc.

\libusepackage is particularly useful in such a preamble.tex when we want to use custom packages that are not part of a TeX distribution, or on CTAN. In this case we commit the respective packages in one of the lib folders and use \libusepackage to load them.

### 5.4 Basic Macros

\sTeXThe \sTeX macro produces this TeX logo. It is provided by the stex-logo package, included with the stex package.

\ifstexhtmlThe TeX conditional \ifstexhtml is _true_ if the current compilation generates HTML, and _false_ otherwise (i.e. generates PDF).

\STEXinvisible\STEXinvisible\STEXinvisible\

Processes \(code\), but does not generate any output. In the HTML, \(code\) is exported with display:none.

Can be used to declare formal content and preserve its semantics in HTML without generating output.

## Chapter Document Features

### Document Fragments

sfragment (_env._): To make reusability of document fragments more feasible, sflex provides the sfragment environment. \begin{segment}[id=\(\langle id\rangle\),short=\(\langle short\ title\rangle\)]{section title} calls \part, \chapter, \section, \subsection, \subsubsection, \paragraph or \subparagraph with argument {section title} depending on the current _section level_ and availability, and increases the level accordingly.

The \(\langle id\rangle\) can be used for cross-document references (see section 6.3).

blindfragment (_env._): In the case where we want to increase the section level _without_ producing a corresponding section header, the blindfragment environment can be used. This allows e.g. typesetting \sections before the first \chapter.

\skipfragment: The \skipfragment macro "skips an sfragment", i.e. it just steps the respective sectioning counter. This macro is useful, when we want to keep two documents in sync structurally, so that section numbers match up: Any section that is left out in one becomes a \skipfragment.

\sectionlevel: The \sectionlevel macro sets the current section level to that provided as argument. This is particularly useful in the preamble of a document, as to be ignored in e.g. \inputref and make sure that sectioning proceeds as desired; e.g. \sectionlevel{section} make sure that the first sfragment will be typeset as a \section (rather than e.g. a \part).

\currentsectionlevel: The \currentsectionlevel macro produces the literal string corresponding to the current section level - e.g. within a chapter (but outside of a section), \currentsectionlevel produces "chapter".

The \Currentsectionlevel macro does the same, but capitalizes the first letter; e.g. in the above situation, \Currentsectionlevel produces "Chapter".

### Using and Referencing Document Fragments

```
inputref{archive}l{(file)}
```

Inputs the file \(file) in \(archive)'s source directory. If \(\{\)_archive_\(\}\)] is empty, the current archive's source directory is used. If there is no current archive, \(file) is resolved relative to the current file.

The file's content is processed within a TeX group when using pdflatex. When converting to HTML however, the file is not processed _at all_, and instead, a reference to the file is inserted, that can be replaced by the HTML generated by the referenced file by e.g. the Mmt system.

This is the recommended method to assemble documents from individual.tex files.

```
\minputref{\inputref,butactuallycall\inputinbothPDFandHTMLmode.Usefulforsmallfragmentsorthosewithoutmodules,butgenerally\inputrefshouldbepreferred.
```

```
\infinputref{\infinputrefisatTeXconditionalforwhetherthecurrentfileiscurrentprocessedviainputref. \infinputref{\(truecode)}l{(falsecode)}} behaveslike \infinputref{\(truecode)}else{falsecode)}f1whenusingpdflatex;inHTMLmodehowever,bothargumentsareprocessedandmarked-upaccordingly,sohostingserver(likeMmt)candynamicallydecidewhichpartstoshoworomit.
```

_If_ the graphix package is loaded,\mhgraphicstakesthesameargumentsas\includgraphics,withtheadditionaloptionalkeyarchive. Itthenresolvesthefilepathin \mhgraphics[archive=some/archive]{some/image}relativetothesource-folderofthesome/archivearchive.Ifnoarchiveisprovided,thefilepathsome/image isresolvedrelativetothecurrentarchive(ifexistent). \cmhgraphicsadditionalwrapstheimageinacenter-environment.

``` \lstininputmllistingLike\mhgraphics,butfor\lstininputlistinginsteadof\lstindependencies.Onlydefinedifthelistingspackageisloaded.

### 6.3 Cross-Document References

If we take features like \inputref and \minput (and thesfragmentenvironment) seriously and build large documents modularly from individually compiling documents for sections, chapters and so on, cross-referencing becomes an interesting problem.

Say, we have a document main.tex, which \inputrefsactionsection1.tex, which references a definition with label some_definition in section2.tex (subsequently also \inputrefed in main.tex). Then the numbering of the definition will depend on the _document context_ in which the document fragment section2.tex occurs - in section2.tex itself (as a standalone document), it might be _Definition 1_, in main.texit might be _Definition 3.1_, and in section1.tex, the definition _does not even occur_, so it needs to be referenced by some other text.

What we would want in that instance is an equivalent of \autoref, that takes the document context into account to yield something like _Definition 1_, _Definition 3.1_ or "_Definition 1 in the section on Foo_" respectively.

For that to work, we need to supply (up to) three pieces of information:

* The _label_ of the reference target (e.g. some_definition),
* (optionally) the _file_/document containing the reference target (e.g. section2). This is not strictly necessary if the reference target occurs in the _same_ document, but if not, we need to know where to find the label,
* (optionally) the document context, in which we want to refer to the reference target (e.g. main).

Additionally, the document in which we want to reference a label needs a title for external references.

```
\sref[archive=\archive1),file=\file1)] {\label)[archive=\archive2),file=\file2),title=(title)]
```

This macro references \(\{\mathit{label}\}\) (declared in \(\langle\mathit{file1}\rangle\) in math archive \(\langle\mathit{archive1}\rangle\)). If the object (section, figure, etc.) with that label occurs (eventually) in the same document, \sref will ignore the second set of optional arguments and simply defer to \autoref if that command exists, or \ref if the hyperref package is not included.

If the referenced object does _not_ occur in the current document however, \sref will refer to it by the object's name as it occurs in the file \(\langle\mathit{file2}\rangle\) in archive \(\langle\mathit{archive2}\rangle\), followed by the title.

In HTML mode, the reference additionally links to the HTML of the file1.9

Footnote 19: The \(\langle\mathit{jobname}\rangle\) is the \(\langle\mathit{jobname}\rangle\).sref, analogous to e.g. the.toc. Note that this consequently requires both file1.tex and file2.tex to have been compiled previously, to generate the.sref file.

For example, doing

```
\sref[file=tutorial/full.en]{sec:basics}[file=tutorial.en,title=the \stex Tutorial] in this very document fragment ([sTeX/Documentation]macros/sref.en.tex) will yield Part I (The Basics) in the \(\langle\mathit{\Sigma}\) Tutorial if compiled itself, or if compiled as part of the \(\langle\mathit{\Sigma}\) manual, and will yield the \(\langle\)autoref link chapter 2 in the documentation (which includes the tutorial).
``` \srefsetin[archive2)]{(file2)}{(title)} ```
Sets a default value for the optional arguments \(\langle\mathit{archive2}\rangle\), \(\langle\mathit{file2}\rangle\) and \(\langle\mathit{title}\rangle\) of \(\langle\)sref. If the second set of optional arguments in \(\langle\)sref are omitted, these default values are used. Particularly useful to set in a preamble.
``` \sreflabel{(\(\langle\mathit{label}\rangle\)) sets a label analogous to \label{\(\langle\mathit{label}\rangle\)}, but for use in \(\langle\)sref.

Note that for every \(\langle\mathit{\Sigma}\) macro or environment that takes an optional id=\(\langle\mathit{id}\rangle\) argument, the \(\langle\mathit{id}\rangle\) (if non-empty) generates an \(\langle\)sreflabel automatically.

For example, \(\langle\)begin\(\{\)sfragment\(\}\)[id=foo]{Foo\(\}\) is equivalent to

```
\sreflabel{foo}.
``````
\extref[archive=\archive1),file=\file1] {\label}}{archive=\archive2),file=(file2),title=(title)}
```

Like \sref, but with the third argument mandatory, \extref will _always_ produce the output as if \label\ would _not_ occur in the current document.

## Chapter 7 Modules and Symbols

### 7.1 Modules

A module is required to declare any new formal content such as symbols or notations (but not variables, which may be introduced anywhere).

\begin{tabular}{l l} module (_env._) & A new module is declared using the basic syntax \\  & begin{smodule}[options]{ModuleName}...\end{tabular}. A module is required to declare any new formal content such as symbols or notations (but not variables, which may be introduced anywhere).

The smodule-environment takes several keyword arguments, all of which are optional:

title (\(\langle\)_token list_\(\rangle\)) to display in customizations.

style (\(\langle\)_string\(\rangle*\)_) for use in customizations, see chapter 9 \\  & id (\(\langle\)_string\(\rangle\)_) for cross-referencing, see \$sreflabel. \\  & ns (\(\langle\)_URI\(\rangle\)_) the namespace to use. _Should not be used, unless you know precisely what you're doing_. If not explicitly set, is computed from the containing file and archive's namespace.

lang (\(\langle\)_language\(\rangle\)_) if not set, computed from the current file name (e.g. foo.en.tex).

sig (\(\langle\)_language\(\rangle\)_) see below.



This is as good a place as any other to explain how $IFX resolves a string symbol to an actual symbol. If \symbol is a semantic macro, then $IFX has no trouble resolving symbolname to the full MMT-URI of the symbol that is being invoked. However, especially in \synname (or if a symbol was introduced using \syndecl* without generating a semantic macro), we might prefer to use the _name_ of a symbol directly for readability - e.g. we would want to write A \synname{natural number} is... rather than A \synname{Nat} is.... $IFX attempts to handle this case thusly: If symbol does _not_ correspond to a semantic macro \symbol and does _not_ contain a?, then $IFX checks all symbols currently in scope until it finds one, whose name is symbol. If symbol is of the form pre?name, $IFX first looks through all modules currently in scope, whose full MMT-URI ends with pre, and then looks for a symbol with name name in those. This allows for disambiguating more precisely, e.g. by saying \synname{Integers?addition} or \synname{RealNumbers?addition} in the case where several additions are in scope.

```
\synname{symbol}{(text)} inMmt/OMDoc generates the term \CMS name="{symbolURI}"/>.
```

```
\synname{pre=(pre),post=(post)}{(symbol)} \SynnameIf the symbol referenced by \(\syntool\) has name name, this is a shortcut for \synref{\(\langle symbol\rangle\}\{(pre)\name{post}\}\). For example, given a symbol group with name abelian group, we can do \synname{pre=Non-,post=s}{agroup} to produce Non-abelian groups. \syn is a shorter variant for \synname; \Synname and \Sn additionally capitalize the first letter. \syn and \$Sn are short for \sn [post=s] and \Sn [post=s], respectively.
``` \srefsymuri{symbol}{(text)}turns \(text) into a link to * The documentation of \(\langle symbol\rangle\), if it occurs in the same document, or * the symbol's documentation online, based on the containing math archive's url-base. \srefsymuri does the same, but expects a symbol's full MMT-URI as first argument. This is particularly useful for e.g. customizing highlighting (see chapter 9).

```
\synuse{\(\langle symbol\rangle\}\) behaves exactly like a semantic macro for \(\langle symbol\rangle\).
```

### 7.4 Notations and Semantic Macros

```
\notation{(symbol)}{(options)}{(code)}
```

introduces a new notation for the referenced symbol.

The starred variant \notation* sets this notation as the (new) default notation.

The optional arguments are:

* prec=\_opprec_);_(_argprec 1_)x...x\_(_argprec n_): An operator precedence and one argument precedence for each argument of the semantic macro. If no argument precedences are given, all argument precedences are equal to the operator precedence. By default, all precedences are 0, unless the symbol takes no argument, in which case the operator precedence is \neginfprec (negative infinity).

```
prec=nobracketsisanabbreviationforprec=\neginfprec;\infprecx...x\infprec.
* op=\(code): An operator notation. If none is given, the notation component marked with \maincomp is used. If no \maincomp occurs in the notation, the default operator notation is \symname{(symbol)}.
* variant=\(id\): An id for this notation. The key variant= can be omitted; i.e. \notation[foo] is equivalent to \notation[variant=foo].
``` \comp isusedtomarknotationcomponentsinax\notationtobehighlighted. Additionally, each notation can use \maincomp at most once to mark the _primary_ notation component. ```
``` \complywouldnotbenecessary:Everythinginapotationthatis_not_anargumentshouldbeaotationcomponent.Unfortunately, itiscomputationallyexpensivetodeterminewhereanargumentbeginsandends, and the argument markers \n maythemselvesbenestedintothermacroapplicationsor\TEXgroups,makingitultimatelyalmostimpossibletodeterminethemautomaticallywhilealsoremainingcompatiblewitharbitraryhighlightingcustomizations(suchastooltips,hyperlinks,colors)thatusersmightemploy,andthatareultimatelyinvokedby\comp.
```

Note that it is required that

1. the argument markers \n neveroccurinsidea\comply,and
2. no semantic macrosmayeveroccurinsideaotation.

Both criteria are not just required for technical reasons, but conceptionally meaningful:

The underlying principle is that the arguments to a semantic macrorepresent_arguments_to_the_mathematicaloperation_represented by a symbol. For example, a semantic macro application \plus{a}{b} wouldrepresent_the actual addition of_(_mathematicalobjects)_a_and_\(b\). It should therefore be impossible for_\(a\)_or_\(b\)_tobepart of a notationcomponent of \plus.

Similarly, a semantic macro can not conceptually be part of the notation of \plus,


6. Since the notation of \mult has no explicitly set argument precedences, SIFX again uses the operator precedence for the arguments of \mult, hence sets \(p_{d}=p_{op}=50\) and recurses. 7. Next, SIFX encounters the inner \plus{c,...} whose notation has \(p_{op}=100\). We compare to the current downward precedence \(p_{d}\) set by \mult, arriving at \(p_{op}=100>50=p_{d}\) - which finally prompts SIFX to insert parentheses, and we proceed as before.

\dobrackets{\(code\)} wraps parentheses around \(\{code\)}.

\withbrackets{\(left\)}{\(right\)}{\(code\)} uses the opening and closing parentheses \(\langle left\rangle\) and \(\langle right\rangle\) for the next pair of parentheses automatically inserted in \(\{\langle code\rangle\}\).

#### Notations for Argument Sequences

The following macros can be used in notations that take mode a or B arguments:

\argsep{\(parameter token\)}{\(separator\)} takes the elements of the argument sequence in position \(\langle parameter token\rangle\) and separates them by \(\langle separator\rangle\).

Note that the first argument _must_ be a parameter token of the form #k, and the argument at position k of the notation has to have argument mode a or B.

\argmap{\(parameter token\)}{\(code\)}{\(separator\)} takes the elements of the argument sequence in position \(\langle parameter token\rangle\), applies the code \(\{\langle code\rangle\}\) to each of them (which therefore should use ##1) and separates them by \(\langle separator\rangle\).

For example, the notation {\(argmap\{\#1}{\{\tt X}^{\{\tt\{\#\#1\}\}\{++\}\}\) applied to the argument {a,b,c} produces \(X^{a}++X^{b}++X^{c}\).

\argarraymap TODO11

#### Semantic Macros

Assume we have a semantic macro \sm macro taking (exemplary) two arguments. The precise behaviour of \sm macro depends on whether we are in text or math mode.

Math Mode\sm macro! produces the default operator notation of its symbol. Without!, \sm macro expects at least two arguments, and \smarco{a}{b}! produces the default notation of its symbol.

If the symbol has a return code, then \smarco{a}{b} continues with executing the return code. Otherwise, \smarco{a}{b} also simply produces the default operator notation.

The starred variants \smarco* and \smarco!* behave as in _text mode_.

**Text Mode**\macro1{_arg_}  marks up _arg_ similarly to how \symref{smarco}{_arg_}  would.

Without the!, \smmacro still only takes a single argument, but it is expected, that within _arg_), the arguments for the symbol are explicitly marked up. The \comp macro is allowed in _arg_) to determine the components of _arg_) to be highlighted.

\arg The \arg macro can be used to explicitly mark the arguments of a semantic macro in text mode.

By default, they are numbered consecutively; e.g. \smmacro{...\arg{a}...\arg{b}} determines a and b to be the (first and second) arguments.

The starred variant \arg* allows for marking up the arguments, but does not produce any output. This can be used to provide arguments that are not mentioned in the text we want to mark up, because they are implicitly obvious or mentioned elsewhere.

If we want to change the order of the arguments, we can provide the precise argument number as an optional argument; e.g. \smmacro{...\arg[2]{a}...\arg[1]{b}} determines b to be the first and a to be the second argument.

An argument number may be used repeatedly, if the corresponding argument mode is a or B.

### 7.5 Simple Inheritance

There are three macros that allow for opening a module, making its contents available for use:

\usemodule\usemodule{_module_} is allowed anywhere and makes the module's contents available up to the current TeX group. This is the right macro to use outside of modules, or when none of its contents use any of the used module's symbols directly (e.g. in types or definientia).

\requiremodule{_module_} is only allowed in modules and makes the required module's contents available within the current module. The imported symbols can be safely used in types and definientia, but not in the return code of symbols, and the imported content is not exported further - i.e. using the current module does not also open the required module.

\importmodule{_module_} is only allowed in modules and makes the required module's contents available within the current module. The imported symbols can be safely used anywhere, and the imported content exported to any modules subsequently importing the current one.

In Mmt, every _document_ and every module induces an Mmt theory. \usemodule induces and Mmt include in the document theory, \importmodule and \requiremodule both induce an include in the module's theory.

It is worth going into some detail how exactly \usemodule, \importmodule and \requiremodule resolve their arguments to find the desired module - which is closely related to the _namespace_ generated for a module, that is used to generate its MMT-URI. Ideally, \STEX would allow for arbitrary MMT-URIs for modules, with no forced relationships between the _logical_ namespace of a module and the _physical_ location of the file declaring it - like Mmt in fact allows for. Unfortunately, \EX only provides very restricted access to the file system, so we are forced to generate namespaces systematically in such a way that they reflect the physical location of the associated files, so that \STEX can resolve them accordingly. Largely, users need not concern themselves with namespaces at all, but for completenesses sake, we describe how they are constructed:

* If \begin{smodule}{Foo} occurs in a file /path/to/file/Foo[._(lang)].tex which does not belong to an math archive, the namespace is file://path/to/file.
* If the same statement occurs in a file /path/to/file/bar[._(lang)].tex, the namespace is file://path/to/file/bar.

In other words: outside of math archives, the namespace corresponds to the file URI with the filename dropped iff it is equal to the module name, and ignoring the (optional) language suffix.

If the current file is in an archive, the procedure is the same except that the initial segment of the file path up to the archive's source directory is replaced by the archive's namespace URI.

Conversely, here is how namespaces/URIs and file paths are computed in import statements, examplary \importmodule:

* \importmodule{Foo} outside of an archive refers to module Foo in the current namespace. Consequently, Foo must have been declared earlier in the same file or, if not, in a file FooI._(lang)].tex in the same directory.
* The same statement _within_ an archive refers to either the module Foo declared earlier in the same file, or otherwise to the module Foo in the archive's top-level namespace. In the latter case, is has to be declared in a file FooI._(lang)].tex directly in the archive's source directory.
* Similarly, in \importmodule{some/path?Foo} the path some/path refers to either the sub-directory and relative namespace path of the current directory and namespace outside of an archive, or relative to the current archive's top-level namespace and source directory, respectively. The module Foo must either be declared in the file \_(top-directory)/some/path/FooI._(lang)].tex, or in \_(top-directory)/some/pathI._(lang)].tex (which are checked in that order).

* Similarly, \importmodule[Some/Archive]{some/path?Foo} is resolved like the previous cases, but relative to the archive Some/Archive in the MathHub directory.

### 7.6 Variables and Sequences

```
\vardef{\vardef{\mname}}{(options)}{\{notation\}}
```

Takes the same arguments as \symdef, but produces a variable rather than a symbol. Variables definitions are always local to the current TeX group and are allowed anywhere (i.e. outside of modules). \_options_) may include the additional keyword bind, in which case the variable will be appropriately abstracted away in statements (see also \varbind).

Unlike \symdef, there is no starred variant \vardef* - variables always generate a semantic macro.

The semantic macro for a variable behaves analogously to that of a symbol.

```
\varnotation{\variable}{\options}{\notation\}
```

Takes the exact same arguments as \notation, but attaches an additional notation to the _variable_ \_variable_ rather than a symbol.

```
\svar[(name)]{(text)}
```

Semantically marks up \_(text)_ as representing a variable \_(name)_. The variable does not need to have been defined prior. If no \_(name)_ is givenm \_(text)_ will be used as the name.

This is useful in situations like "throwaway expressions" or remarks; e.g.

```
\varseq{\varseq{\mname}}{\options}{\range}{\notation\}
```

Declares a new variable sequence. The \_(options)_ are the same as for \vardef. If not provided, args=1 by default (a 0-ary sequence would just be a normal variable).

A type (given as type=) is interpreted to be the type of every element \(a_{i}\) of the sequence \(a_{1},...,a_{n}\) (not of the sequence itself). If the type is itself a sequence \(A_{1},...,A_{n}\), the assumption is that its range is the same as the one of the new sequence, and the type of every \(a_{i}\) in the sequence is \(A_{i}\).

\(\_range\) needs to be a comma-separated sequence of either args many arguments, or \ellipses.

The resulting semantic macro is allowed anywhere SLEX expects an argument mode a or B argument.



Note the insertion of! behind the A - this is to make sure that assignments to semantic macros that takes arguments don't accidentally eat more than they should.

Also note that multiple assignments can be done in the same pair of [], or chained - i.e. both $\struct[fielda=A,fieldb=B]...$ and $\struct[fielda=A][fieldb=B]...$ are valid and equivalent. $\struct[fielda=A,fielda=B]...$ however is not - every field may be assigned at most once.

## Chapter 8 Statements

The _sdefinition_ environment represents (primarily mathematical) _definitions_; in particular for symbols. The contents of the environment will be used as _documentation_ for any symbol that either orrus as a \definition(or \definance) within the \definition, or that is listed in the optional for= argument of the environment.

If a \definiens occurs, this will be used by MMT as the formal definiens for the respective symbol.

The _sassertion_ environment represents _assertions_, i.e. propositions such as _theorems_, _lemma_, _axioms_, etc. If a \conclusion occurs within the \assertion, its argument will be used as the formal _statement_ of the assertion.

The _sexample_ environment represents examples (or counterexamples).

The _sparagraph_ environment represents all other kinds of (logical) paragraphs, such as remarks, comments, transitions bwetween topics, recaps, reminders, etc.

All of these take the same arguments:

* for=\(\mathit{csl}\): a comma-separated list of symbols.
* The same optional arguments as \symdecl, with macro= replacing the name of the semantic macro. All of them are only relevant, if either name= or macro= are provided. As with \symdecl, if no name is given, but macro is, then the same name is used for both the semantic macro and the symbol itself. If name is given but macro isn't, no semantic macro is generated. Subsequently, the newly generated symbol is added the for-list.
* style: see chapter 9.
* title: a title to use in various styles (see chapter 9).
* id: a label to use for \sref.


More on Assertions

```
premise The \conclusionmacro can be used to mark up the actual statement within an assertion. The \premise macro can be used to additionally mark up _premises_.

If the sassertion environment has several elements in its for list, an optional argument \conclusion[(_symbol_)]{...} can be used to tell \SEX which symbol's statement this is. By default, the _first_ symbol in the for list is used.

Here is how Mmt will treat the fragments marked up with \conclusion and \premise:

Firstly, it will attempt to translate the contents of \conclusion into an Mmt/OM-Doc term \(c\). This succeeds easily if the \conclusion is some semantic macro (applied to arguments).

Secondly, it will collect all fragments marked up with \premise and do the same to them \((p_{1},...,p_{n})\).

It will then check, whether a symbol is in scope, that has role=implication. If so, it will use that implication symbol to attach all the premises to the conclusion, resulting in \(t:=\imply(p_{1},...,p_{n},c)\).

Next, it will check for all variables currently in scope, that were defined with the optional argument bind. It then will check, whether a symbol is in scope, that has role=forall. If so, it will use that forall symbol to bind all these variables (in the order in which they were defined) in the term \(t\).

Finally, it will check, whether a symbol is in scope, that has role=judgment. If so, it will set \(t:=\judgment(t)\).

If no forall symbol is found, it will first apply the judgment symbol (if existent) and then use the bind symbol that ships with \SEX to bind the variables.

The final term will be attached as type to the corresponding Mmt constant, if it was declared in the same module as the \definiens occurrence.
``` sproof(env.) TODO12 ```


} deflsymrefemph#1{% \ifcsnametextcolor}endcsname \textcolor{teal}{#1}% \else#1{fi } } ```
``` compemph Like\symrefemphand\symrefemph@uri,butgovernsthehighlightingofcomponents(markedwith\compor\maincomp)innotations.
```

```
defemph Like\symrefemphand\symrefemph@uri,butgovernsthehighlightingofdefiniendamarkedwith\definitiond(or\defname).
```

```
varemph Like\compemphand\compemph@uri,butgovernsthehighlightingofcomponents(markedwith\compor\maincomp)innotationsofvariables.
```

The second argument to \varemph@uri is the _name_ of the variable.

### 9.2 Styling Environments and Macros

A variety of environments and macros provided by \(\$\$\)EX are _stylable_ using the macros \stexstyle\(\{\)_name_\(\}\)[_style_]{...}. These stylable environments and macros bind various of their parameters to macros \this\({\)_parameter_\(}\), which can then be used in the styles.

For example, if we have a definition environment that we would want to use to style our definitions, we can do (in the simplest case)

```
\stexstyledefinition{\begin{definition}}{\{end{definition}}}
```

This tells \(\$\$\)EX to insert \begin{definition} at the beginningofeverydefinitionenvironment, and \end{definition} at the end.

If we have a environments theorem and lemma, we probably want the sassertion environment to use those for theorems and lemma. We can achieve that by doing

```
\stexstyleassertion[theorem]{\begin{theorem}}{\{end{theorem}}} \stexstyleassertion[lemma]{\begin{lemma}}{\{end{lemma}}}
```

Now if we do \begin{sassertion}[style=theorem],itwillwraptheenvironmentwith\begin{theorem}...\end{theorem}.

Of course, many such statements might have a title, as e.g. in

**Theorem 9.2.1** (Godel's First Incompleteness Theorem).:...

In sasssertion, we can provide that title as optional argument using title=.... Before calling the styling provided, sassertion will store that title in the macro \thistitle, which we can use in the styling. For example, we might prefer to pass it on to the theorem environment:

``` \stexstyleassertion[theorem]{\ifx\thistitle\@empty \begin{theorem}\else\begin{theorem}[\{thistitle\


## Chapter 10 Additional Packages

### 10.1 NotesSlides Manual

#### Introduction

The notesslides document class is derived from beamer.cls [**beamerclass:on**], it adds a "notes version" for course notes that is more suited to printing than the one supplied by beamer.cls.

The notesslides class takes the notion of a slide frame from Till Tantau's excellent beamer class and adapts its notion of frames for use in the SIFX and OMDoc. To support semantic course notes, it extends the notion of mixing frames and explanatory text, but rather than treating the frames as images (or integrating their contents into the flowing text), the notesslides package displays the slides as such in the course notes to give students a visual anchor into the slide presentation in the course (and to distinguish the different writing styles in slides and course notes).

In practice we want to generate two documents from the same source: the slides for presentation in the lecture and the course notes as a narrative document for home study. To achieve this, the notesslides class has two modes: _slides mode_ and _notes mode_ which are determined by the package option.

#### Package Options

The notesslides class takes a variety of class options:

* The options slides and notes switch between slides mode and notes mode (see subsection 10.1.3).
* If the option sectocframes is given, then for the sfragments, special frames with the sfragment title (and number) are generated.
* If the option frameimages is set, then slide mode also shows the \frameimage-generated frames (see 10.1.3). If also the fiboxed option is given, the slides are surrounded by a box.

#### Notes and Slides

frame(_env._) Slides are represented with the frame environment just like in the beamer class, see [**Tantau:ugbc**] for details.

note(_env._) The notesslides class adds the note environment for encapsulating the course note fragments.

Note that it is essential to start and end the notes environment at the start of the line - in particular, there may not be leading blanks - else LaTeX becomes confused and throws error messages that are difficult to decipher.

By interleaving the frame and note environments, we can build course notes as shown here:

```
1\ifnotes\maketitle\else
2\frame[noframenumbering]\maketitle\fi
3
4\begin{note}
5We start this course with...
6\end{note}
7
8\begin{frame}
9\frametitle{The first slide}
10\...
11\end{frame}
12\begin{note}
13\dots and more explanatory text
14\end{note}
15
16\begin{frame}
17\frametitle{The second slide}
18\dots
19\end{frame}
20\dots
```

``` \ifnotesNote the use of the \ifnotes conditional, which allows different treatment between notes and slides mode - manually setting \notestrue or \notesfalse is strongly discouraged however.

We need to give the title frame the noframenumbering option so that the frame numbering is kept in sync between the slides and the course notes.

The beamer class recommends not to use the allowframebreaks option on frames (even though it is very convenient). This holds even more in the notesslides case: At least in conjunction with \newpage, frame numbering behaves funnily (we have tried to fix this, but who knows).

* If we want to transclude a the contents of a file as a note, we can use a new variant \inputref* of the \inputref macro: \inputref*{foo} is equivalent to \begin{note}\inputref{foo}\end{note}.
* There are some environments that tend to occur at the top-level of note environments.
* We make convenience versions of these: e.g. the nparagraph environment is just an ndefinition (_env._) separation inside a note environment (but looks nicer in the source, since it avoids one example (_env._) level of source indenting). Similarly, we have the nfragment, nddefinition, nexample, nsproof, and nassertion environments.

#### Customizing Header and Footer Lines

The notesslides package and class comes with a simple default theme named sTeX that provided by the beamterthemesTeX. It is assumed as the default theme for SLEX-based notes and slides. The result in notes mode (which is like the slides version except that the slide hight is variable) is

* The default logo provided by the notesslides package is the SLEX logo it can be customized using \setslidelogo{_logo name_}.
* The default footer line of the notesslides package mentions copyright and licensing. In notesslides source stores the author's name as the copyright holder. By default it is the author's name as defined in the \author macro in the preamble. \setsource{_name_} can change the writer's name.
* For licensing, we use the Creative Commons Attribution-ShareAlike license by default to strengthen the public domain. If package hyperref is loaded, then we can attach a hyperlink to the license logo. \setlicensing[_{url}_{l}\{_{logo name}_{}}\) is used for customization, where \(\langle url\rangle\) is optional.

#### Frame Images

Sometimes, we want to integrate slides as images after all - e.g. because we already have a PowerPoint presentation, to which we want to add SLEX notes.


\setSGvar{\setSGvar{\_vname_}}{(_text_)} to set the global variable \_vname_} to \_text_ and \usesSGvar{\_vname_}}.

\useSGvar to reference it.

\ifSGvarWith\ifSGvar we can test for the contents of a global variable: the macro call \ifSGvar{\_vname_}}{\(\{\)_val_}}{\(\{\)_ctext_}}{\(\}\) tests the content of the global variable \(\langle\)_vname_\(\rangle\), only if (after expansion) it is equal to \(\langle\)_val_\(\rangle\), the conditional text \(\langle\)_ctext_\(\rangle\) is formatted.

#### Excursions

In course notes, we sometimes want to point to an "excursion" - material that is either presupposed or tangential to the course at the moment - e.g. in an appendix. The typical setup is the following:

```
1\excursion{founif}{../fragments/founif.en}
2{Wewillcoverfirst-orderunificationin}
3...
4\begin{appendix}\printexcursions\end{appendix}
```

It generates a paragraph that references the excursion whose source is in the file.../fragments/founif.en.tex and automatically books the file for the \printexcursions command that is used here to put it into the appendix. We will look at the mechanics now.

\excursionThe \excursion{\_ref_}}{(_path_)}{(_text_)} is syntactic sugar for

```
1\begin{inparagraph}{title=Excursion}
2\activateexcursion{founif}{../ex/founif}
3Wewillcoverfirst-orderunificationin\sref{founif}.
4\end{appagraph}
```

\activateexcursion{\_path_} augments the \printexcursions macro by a call \inputref{\_path_}. In this way, the \printexcursions macro (usually in the appendix) will collect up all excursions that are specified in the main text.

Sometimes, we want to reference - in an excursion - part of another. We can use \excursionref{\_label_} for that.

\excursiongroupFinally, we usually want to put the excursions into an sfragment environment and add an introduction, therefore we provide the a variant of the \printexcursions macro: \excursiongroup[id=\(id),intro=\(\_path\)] is equivalent to

```
1\begin{note}
2\begin{sfragment}[id=<id>]{Excursions}
3\inputref{\_path>}
4\printexcursions
5\end{table} \begin{table} \begin{table} \begin{table} 
\begin{table}
\begin{tabular}{l} \hline \hline \(\backslash\)setSGvar\{\_vname_}}{\{\(\backslash\)setSGvar{\_vname_}}}{\When option book which uses \pagestyle{headings} is given and semantic macros are given in the sfragment titles, then they sometimes are not defined by the time the heading is formatted. Need to look into how the headings are made. This is a problem of the underlying document-structure package.

Local Variables: mode: latex TeX-master:../stex-manual End:

### 10.2 Problem Manual

#### Introduction

The problem package supplies an infrastructure that allows specify problem. Problems are text fragments that come with auxiliary functions: hints, notes, and solutions15. Furthermore, we can specify how long the solution to a given problem is estimated to take and how many points will be awarded for a perfect solution.

Footnote 15: for the moment multiple choice problems are not supported, but may well be in a future version

Finally, the problem package facilitates the management of problems in small files, so that problems can be re-used in multiple environment.

#### Problems and Solutions

The problem package takes the options solutions (should solutions be output?), notes (should the problem notes be presented?), hints (do we give the hints?), gnotes (do we show grading notes?), pts (do we display the points awarded for solving the problem?), min (do we display the estimated minutes for problem soling). If theses are specified, then the corresponding auxiliary parts of the problems are output, otherwise, they remain invisible.

The boxed option specifies that problems should be formatted in framed boxes so that they are more visible in the text. Finally, the test option signifies that we are in a test situation, so this option does not show the solutions (of course), but leaves space for the students to solve them.

problem (_env._): The main environment provided by the problempackage is (surprise surprise) the problem environment. It is used to mark up problems and exercises. The environment takes an optional KeyVal argument with the keys id as an identifier that can be reference later, pts for the points to be gained from this exercise in homework or quiz situations, min for the estimated minutes needed to solve the problem, and finally title for an informative title of the problem.

**Example 18**: Input:* The solution environment can be to specify a solution to a problem. If the package option solutions is set or \solutionstrue is set in the text, then the solution will be presented in the output. The solution environment takes an optional KeyVal argument with the keys id for an identifier that can be reference for to specify which problem this is a solution for, and height that allows to specify the amount of space to be left in test situations (i.e. if the test option is set in the \usepackage statement). hint (_env._) The hint and exnote environments can be used in a problem environment to give hints and to make notes that elaborate certain aspects of the problem. The gnote (grading gnote (_env._) notes) environment can be used to document situations that may arise in grading.
* Sometimes we would like to locally override the solutions option we have given to the package. To turn on solutions we use the \startsolutions, to turn them off, \stopsolutions. These two can be used at any point in the documents.
* Also, sometimes, we want content (e.g. in an exam with master solutions) conditional on whether solutions are shown. This can be done with the \ifsolutions conditional.

#### Markup for Added-Value Services

The problem package is all about specifying the meaning of the various moving parts of practice/exam problems. The motivation for the additional markup is that we can base added-value services from these, for instance auto-grading and immediate feedback.


In "exam mode" where disable solutions (here via \stopsolutions)

**Example 20**

Input:

```
1\stopsolutions
2\begin{problem}{title=Functions,name=functions1}
3Whatisthekeywordtointroduceafunctiondefinitioninpython?
4\begin{mcb}
5\mcc[T]{def}
6\mcc[F,feedback=thatisforCandC++]{function}
7\mcc[F,feedback=thatisforStandardML]{fun}
8\mcc[F,Ftext=Nooooooooo,feedback=thatisforJava]{publicstaticvoid}
9\end{mcb}
10\end{problem}
```

Output:

```
**Exercise (Functions)**

Whatisthekeywordtointroduceafunctiondefinitioninpython?

\begin{mcb}
11\end{mcb}
12\end{mcb}
```

wegetthequestionswithoutsolutions (thatiswhatthestudentsseeduringtheexam/quiz).

#### Filling-In Concrete Solutions

The next simplest situation, where we can implement auto-grading is the case where we have fill-in-the-blanks


#### Including Problems

The \includeproblem macro can be used to include a problem from another file. It takes an optional KeyVal argument and a second argument which is a path to the file containing the problem (the macro assumes that there is only one problem in the include file). The keys title, min, and pts specify the problem title, the estimated minutes for solving the problem and the points to be gained, and their values (if given) overwrite the ones specified in the problem environment in the included file.

The sum of the points and estimated minutes (that we specified in the pts and min keys to the problem environment or the \includeproblem macro) to the log file and the screen after each run. This is useful in preparing exams, where we want to make sure that the students can indeed solve the problems in an allotted time period.

The \min and \pts macros allow to specify (i.e. to print to the margin) the distribution of time and reward to parts of a problem, if the pts and pts options are set. This allows to give students hints about the estimated time and the points to be awarded.

#### Testing and Spacing

The problem package is often used by the hwexam package, which is used to create homework assignments and exams. Both of these have a "test mode" (invoked by the package option test), where certain information -master solutions or feedback - is not shown in the presentation.

\testspace \testspace takes an argument that expands to a dimension, and leaves vertical space accordingly. Specific instances exist: \testssmallspace, \testssmallspace, \testssmallspace give small (1cm), medium (2cm), and big (3cm) vertical space.

\testssmallspace \testnewpage makes a new page in test mode, and \testemptypage generates an \testemppage empty page with the cautionary message that this page was intentionally left empty.

\testemptype Local Variables: mode: latex TeX-master:../stex-manual End:

LocalWords: solutions,notes,hints,gnotes,pts,min,boxed,testgnotes elefants,ptsgnote LocalWords: 2,title exnote hint,exnote,gnote ifsolutions mcb keyvals Ttext Flext LocalWords: Functions,name F,feedback Noooooooooo,feedback 2,title includeproblem LocalWords: elefants.fillin,title

### 10.3 HWExam Manual

#### Introduction

The hwexam package and class supplies an infrastructure that allows to format nice-looking assignment sheets by simply including problems from problem files marked up with the problem package. It is designed to be compatible with problems.sty, and inherits some of the functionality.

##### 10.3.2 Package Options

The hwexam package and class take the options solutions, notes, hints, gnotes, pts, min, and boxed that are just passed on to the problems package (cf. its documentation for a description of the intended behavior).

Furthermore, the hwexam package takes the option multiple that allows to combine multiple assignment sheets into a compound document (the assignment sheets are treated as section, there is a table of contents, etc.).

Finally, there is the option test that modifies the behavior to facilitate formatting tests. Only in test mode, the macros testspace, \testnewpage, and \testemptypage have an effect: they generate space for the students to solve the given problems. Thus they can be left in the LaTeX source.

##### 10.3.3 Assignments

This package supplies the assignment environment that groups problems into assignment sheets. It takes an optional KeyVal argument with the keys number (for the assignment number; if none is given, 1 is assumed as the default or -- in multi-assignment documents title -- the ordinal of the assignment environment), title (for the assignment title; this is type referenced in the title of the assignment sheet), type (for the assignment type; e.g. "quiz", given or "homework"), given (for the date the assignment was given), and due (for the date the assignment is due).

##### 10.3.4 Including Assignments

The \inputassignment macro can be used to input an assignment from another file. It takes an optional KeyVal argument and a second argument which is a path to the file containing the problem (the macro assumes that there is only one assignment environment in the included file). The keys number, title, type, given, and due are just as for the assignment environment and (if given) overwrite the ones specified in the assignment environment in the included file.

##### 10.3.5 Typesetting Exams

The \testheading takes an optional keyword argument where the keys duration specifies a string that specifies the duration of the test, min specifies the equivalent in number min of minutes, and reqpts the points that are required for a perfect grade.

 reqpts1 \title{320101 General Computer Science (Fall 2010)}  2 

Will result in

**320101 General Computer Science (Fall 2010)**

2023-03-21

**You have one hour (sharp) for the test**;

Write the solutions to the sheet.

The estimated time for solving this exam is 10 minutes, leaving you

50 minutes for revising your exam.

You can reach 10 points if you solve all problems. You will only need

27 points for a perfect score, i.e. -17 points are bonus points.

_You have ample time, so take it slow and avoid rushing_

_to mistakes!_

_Different problems test different skills and knowledge, so_

_do not get stuck on one problem._

\begin{tabular}{|l|c|c|c|c|c|c|c|c|c|} \hline  & \multicolumn{4}{|c|}{To be used for grading, do not write here} & \multicolumn{1}{|c|}{} \\ \hline prob. & 4.1 & 1.1 & 1.2 & 2.1 & 2.2 & 2.3 & 2.4 & 2.5 & Su \\ \hline total & 0 & 0 & 0 & 10 & 0 & 0 & 0 & 0 & 10 \\ \hline reached & & & & & & & & & & \\  & & & & & & & & & & \\  & & & & & & & & & & \\ \hline \end{tabular}

good luck

17

Local Variables: mode: latex TeX-master:../stex-manual End:

LocalWords: hwexam solutions,notes,hints,gnotes,pts,min gnotes testemptpage re-

qpts LocalWords: inputassignment reqpts hour,min 60,reqpts

### 10.4 Tikzinput Manual

The selective input functionality of the tikzinput package assumes that the TIKZ pictures are externalized into a standalone picture file, such as the following one

```
1\documentclass{standalone} 2\usepackage{tikz} 3\usetikzpackage{...} 4\begin{document} 5\begin{tikzpicture} 6... 7\end{tabular}
```

The standalone class is a minimal LaTeX class that when loaded in a document that uses the standalone package: the preamble and the documenat environment are disregarded during loading, so they do not pose any problems. In effect, an \input of the file above only sees the tikzpicture environment, but the file itself is standalone in the sense that we can run LaTeX over it separately, e.g. for generating an image file from it.

```
\tikzinput
```

This is exactly where the tikzinput package comes in: it supplies the \tikzinput macro, which - depending on the image option - either directly inputs the TIKZ picture (source) or tries to load an image file generated from it.

Concretely, if the image option is not set for the tikzinput package, then \tikzinput[(_opt_)]{(_file_)} disregards the optional argument \(_opt_) and inputs (_file_).tex via \input and resizes it to as specified in the width and height keys. If it is, \tikzinput[(_opt_)]{(_file_)} expands to \includegraphics[(_opt_)]{(_file_)}. \ctizkinput is a version of \tikzinput that is centered.

``` \mhtikzinput is a variant of \tikzinput that treats its file path argument as a relative path in a math archive in analogy to \inputref. To give the archive path, we use the mhrepos= key. Again, \cmhtizkinput is a version of \mhtikzinput that is centered.

Sometimes, we want to supply archive-specific TIKZ libraries in the lib folder of the archive or the meta-inf/lib of the archive group. Then we need an analogon to \libinput for \usettikzlibrary. The \tex-tikzinput package provides the libusetikzlibrary for this purpose.

Local Variables: mode: latex TeX-master:../stex-manual End:

## Part III Documentation

## Chapter 11 SIEX Developer Manual

\(\star\) indicates fully expandable functions, which can be used within an \(\mathbf{x}\)-type argument (in plain TeX terms, inside an \(\mathtt{\char 94}\)def), as well as within an \(\mathtt{f}\)-type argument. \(\ddagger\) indicates restricted expandable functions, which can be used within an \(\mathbf{x}\)-type argument but cannot be fully expanded within an \(\mathtt{f}\)-type argument. \(\underline{\mathit{TF}}\) indicates conditional (\(\mathtt{if}\)) functions whose variants with \(\mathtt{T}\), \(\mathtt{F}\) and \(\mathtt{TF}\) argument specifiers expect different "true"/"false" branches.

\(\mathtt{\char 94}\)stex_debug:nn \(\mathtt{\char 94}\)(prefix)\(\mathtt{\char 94}\)(msg)\(\mathtt{\char 94}\)Logs the debug message \(\mathtt{\char 94}\)(msg)\(\mathtt{\char 94}\) under the prefix \(\mathtt{\char 94}\)(prefix)\(\mathtt{\char 94}\). A message is shown if its prefix is in a list of prefixes given either via the package option debug=\(\langle\)prefixes\(\rangle\) or the environment variable STEX_DEBUG=\(\langle\)prefixes\(\rangle\), where the latter overrides the former.




\stex_get_symbol:n \l_stex_get_symbol_mod_str \l_stex_get_symbol_name_str \l_stex_get_symbol_arity_int \l_stex_get_symbol_args_tl \l_stex_get_symbol_def_tl \l_stex_get_symbol_type_tl \l_stex_get_symbol_return_tl \l_stex_get_symbol_invoke_cs \stex_get_symbol:n attemps to find a symbol with the given name or id that is currently in scope. A name may be prefixed with a module name/path separated by?.

Throws an error if no such symbol is found; otherwise, sets the listed \l_stex_get_symbol_...- macros to the components of the found symbol.

\stex_if_check_terms_p: * whether to typeset declaration components (notations, types, definientia etc.) in a throwway box. Is true iff the backend is pdflatex and either the STEX_CHECKTERMS environment variable or checkterms package option is set.

\stex_check_term:n typesets the argument in a throwaway box in math mode iff \stex_if_check_terms: is true.

Is deactivated in sms-mode.

\stex_symbolcl_do: \stex_key_name_str \l_stex_key_args_str \l_stex_key_args_str \l_stex_key_argnames_clist \l_stex_key_argnames_clist \l_stex_key_argnames_seq \stex_symbol_arity_int: the arity of the symbol,

\l_stex_key_args_str: the args string as a definite sequence of argument-mode characters, whose length is the arity of the symbol; e.g. 3 is turned into iii,

\l_stex_assoc_args_count: the number of sequence arguments (i.e. a or B mode),

\l_stex_argnames_seq: the full sequence of argument names; those not provided by \l_stex_key_argnames_clist are set to be $j, where j is the index of the argument,

\l_stex_get_symbol_args_tl: a token list of triples \m{_(\(\mathit{argmax})\}\), where j is the index and m the respective argument mode character (i.e. i, a, b or B).



argument positions for semantic extractions, but we should adhere to the default LaTeX category code scheme in doing so.

```
\STEXInternalTermMathArgiii ASTEXInternalTermMathAssocArgiiiiii SIETInternalAssocArgMarkerI STEXInternalAssocArgMarkerII STEXInternalTermMathOMSOrOMViii ASTEXInternalTermMathOMAiii ASTEXInternalTermMathOMBiii ASTEXInternalSymbolAfterInvovkationTL
```

In OpenMath/OMDoc, there are (for our purposes) three kinds of expressions that an application of a semantic macro - and hence a notation macro - can represent, each of which corresponds to a macro taking care of the semantic annotations:

* OMS/OMV: a simple symbol (arity 0) (\STEXInternalTermMathOMSOrOMViii)
* OMA: an application of a symbol to argument (arity \(>\) 0, \STEXInternalTermMathOMAiii)
* OMB: a binding application of a symbol that binds/declares one or more variables (argument string contains b or B, \STEXInternalTermMathOMBiii).

The arguments are marked with \STEXInternalTermMathArgii (i or b) or \STEXInternalTermMathAssocArgiiiiii (a or B). Finally, the notation is closed with \STEXInternalSymbolAfterInvovkationTL.

How this works is best explained by example.

**Example 23**: Assume we have a symbol and notation:

```
\ysmdecl{somesymbol}[args=iai] \notation{somesymbol}[prec=10;20x30x40,variant=foo]
3{First: #1; Second: #2; Third: #3; End}
4{(#1 -- ##1 split #2 -- #3)}
```

Since the symbol corresponds to an OMA, the whole notation is wrapped in \STEXInternalTermMathOMAiii, taking as arguments the variant identifier (foo), the operator precedence (10) and the body of the notation.

The second argument in the notation, being associative, is wrapped in a \STEXInternalTermMathAssocArgiiii, taking as arguments the argument number (2), the precedence (30), the TeX parameter token (#2) the notation body ((#1 -- #1 split #2 -- #3)), and finally the argument mode (a). Additionally, the markers ##1 and #2 are replaced by \STEXInternalAssocArgMarkerI and \STEXInternalAssocArgMarkerII, respectively.

Subsequently, the non-sequence parameter tokens are wrapped in \STEXInternalTermMathArgiiii, with arguments mj (where m is the mode und j the index), the precedence (20 or 40 respectively), and the parameter token.

Finally, a \STEXInternalSymbolAfterInvokationTL is inserted.

The final expansion of \l_stex_notation_macrocode_cs is thus:

```
\STEXInternalTermMathOMAiii{foo}{10}{2First: \STEXInternalTermMathArgiiii{i1}{20}{#1};
```
3Second: \STEXInternalTermMathAssocArgiiii{2}{30}{#2}{4} (\STEXInternalTermMathArgiiii{i1}{20}{#1} --```
1\stex_notation_top:nnw{(symboluri)}{(code)}calls\stex_notation_parse_and_then:nw{(code)}and, adds the notation for the symbol with URI (symboluri) to the current module and exports it to the HTML (if applicable).

### 11.5 Structural Features
```
1stex_structural_feature_module:nn\stex_structural_feature_module_end:\stex_structural_feature_module:nn{(name)}{(typeid)}
2\g_stex_last_feature_str ```

opens a new module-like structural feature of type (_typeid_) with name (_name_), which needs to be closed with \stex_structural_feature_module_end:.

Its body behaves like a nested module with name (_modulename_)/\name_), the full URI of which is stored in \g_stex_last_feature_str for subsequent elaboration.

\list_startvariant_feature_morphism:nnnnnn \user_structural_feature_morphism_end: {(moprhismname)}{(typeid)}{(archive)}{(domain)}{(annotations)} \list_start_name_str \list_morphism_symbols_prop \list_exprorphism_renames_prop \list_exprorphism_morphisms_seq opens a new morphism-like structural feature of type \(\langle\)_typeid_\(\rangle\) with name \(\langle\)_morphismname_\(\rangle\) and the module \([\{(archive)\}]{(domain)\}\) as domain, which needs to be closed with \stex_structural_feature_morphism_end:

Deactivates \symdecl, \textsymdecl, \symdef, \notation and \module, and activates \assign, \assignMorphism and \renamedecl.

Defines the following macros:

* \l_stex_feature_name_str ={\(name)}.
* \l_stex_current_domain_str = the full uni of \(\langle\)_domain_\(\rangle\).
* \l_stex_morphism_symbols_prop: This property list is initialized as follows: For every symbol transitively included in \(\langle\)_domain_\(\rangle\) with data \(\langle\)_module_\(\rangle\), \(\langle\)_name_\(\rangle\), \(\langle\)_id_\(\rangle\), \(\langle\)_arity_\(\rangle\), \(\langle\)_args_\(\rangle\), \(\langle\)_definiens_\(\rangle\), \(\langle\)_type_\(\rangle\), and \(\langle\)_return code_\(\rangle\), the property list contains an entry with key \([\{(module)\}]{(\Gamma(name)\}]\) and value \(\{\langle\)_id_\(\rangle\}{\Gamma(arity)\}{\{(args)\}{(definiens)\}}\){(\(type)\}{(return\) code)}.
* \(\l\)l_stex_morphism_renames_prop: An initially empty property list.
* \(\lhd\)_stex_morphism_morphisms_seq: TODO

At \(\l\)stex_structural_feature_morphism_end:, the elaboration is computed from the above data thusly:

For every entry in \l\l\_stex_morphism_symbols_prop, a new symbol is created with the values \(\langle\)_arity_\(\rangle\), \(\langle\)_args_\(\rangle\), \(\langle\)_definiens_\(\rangle\), \(\langle\)_type_\(\rangle\) and \(\langle\)_return code_\(\rangle\) from that property list, and either:

* if \(\lhd\)_stex_morphism_renames_prop does _not_ contain an entry with key \(\langle\)_module_\(\rangle\)?\(\langle\)_name_\(\rangle\), then the elaborated name is \(\langle\)_morphismname_\(\rangle\)/\(\langle\)_name_\(\rangle\) and its \(\langle\)_id_\(\rangle\) is empty (no semantic macro is generated), or
* if \(\lhd\)_stex_morphism_renames_prop contains an entry with key \(\langle\)_module_\(\rangle\)?\(\langle\)_name_\(\rangle\), then its value needs to be of the form \(\{\langle\)_id_\(\rangle\}{\Gamma(name)\}\), which are used for the elaborated symbol.

All notations of the symbols transitively included in the domain are copied over to their elaborations.



##### Optional (Key-Value) Argument Handling

LIFEX3 is surprisingly weak when it comes to handling optional (key-val) arguments in such a manner that _only_ the freshly set macros are defined, and to modularly build up sets of argument keys. The following macros attempt to fix that:

```
\stex_keys_define:nnnn{\stex_keys_set:nn}{\stex_keys_define:nnnn{\stex_keys_define:nnnn}{\stex_keys_define:nnnn}{\stex_keys_define:nnnn}{\stex_keys_set:nn}
```

Defines a set of keys and their allowed values with identifier \stex/\(id\), that inherits from the sets with identifiers in \(\langle\)_parents_\(\rangle\).

\stex_keys_set:nn{\(id\)}{\(\langle\)_CSL\(\rangle\)} first executes \(\langle\)_setup code_\(\rangle\) (e.g. to empty the macros holding the values) and then sets the keys in set \(\langle\)_id_\(\rangle\) with the values provided in \(\langle\)_CSL_\(\rangle\).

```
\_stex_do_id: should be called whenever a macro or environment has a label id, i.e. calls \stex_keys_set:nn{id}{...}, after the title has been typeset. Sets a \label by calling \stex_ref_new_doc_target:n{\(id\)}.
``` \stex_keys_define:nnnn{archivefile}{\stex_clear:N\l_stex_key_archive_str}{\stex_clear:N\l_stex_key_file_str}{\stex_strset_x:N=\l_stex_key_archive_str,
6file.str_set_x:N=\l_stex_key_file_str}{id} ```

then calling \stex_keys_set:nn{archivefile}{id=foo,file=bar} sets \l_stex_key_file_str={bar}, assures that \l_stex_key_archive_str is empty, and executes the code associated with id, i.e. it sets \l_stex_key_id_str={foo}.












## Chapter 12 Additional Packages

### 12.1 NotesSlides Documentation

todo

### 12.2 Problem Documentation

todo

### 12.3 HWExam Documentation

todo

### 12.4 Tikzinput Documentation

todo

## Part IV Implementation

## Chapter 13 The SIFX Implementation

### 13.1 Setting up

Setup code for the document class

```
1\(\langle\)*cls\(\rangle\)
2%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% stex.dtx%%%%%%%%%%%%%%%%%%%%%%%%%%
3
4\RequirePackage{expl3,13keys2e}
5\ProvidesExplClass{stex}{2023/03/19}{3.3.0}{sTeXdocumentclass}
6
7\DeclareOption*{\PassOptionsToPackage{\CurrentOption}{stex}}
8\ProcessOptions
9
10\RequirePackage{stex}
11
12\LoadClass{article}
13\(\langle\)/cls\(\rangle\)
```

Setup code for the package

```
14\(\langle\)*package\(\rangle\)
15\RequirePackage{expl3,13keys2e,ltxcmds}
16\ProvidesExplPackage{stex}{2023/03/19}{3.3.0}{sTeXpackage}
17\RequirePackage{stex-logo} % externalized for backwards-compatibility reasons
18\RequirePackage{standalone}
19
20\message{~~J*-This-is-sTeX-version-3.3.0-*~~J}
```

Package options:

```
21\keys_define:nn{stex/package}{
22debug.str_set_x:N=\c_stex_debug_clist,
23lang.clist_set:N=\c_stex_languages_clist,
24mathhub.tl_set_x:N=\mathhub,
25usesms.bool_set:N=\c_stex_persist_mode_bool,
26writesms.bool_set:N=\c_stex_persist_write_mode_bool,
27checkterms.bool_set:N=\c_stex_check_terms_bool,
28image.bool_set:N=\c_tikzinput_image_bool,
29unknown.code:n={}
30}
```* %exp_args:NNo\clist_set:Nn\c_stex_debug_clist\c_stex_debug_clist
* %ProcessKeysOptions{stex/package} Errormessages:
* %input{stex-en.ldf}

### 13.2 Utilities

* %cs_set_eq:NN\stex_undefined:\undefined

#### Calling kpsewhich and Environment Variables

* %(@0=stex_envs)
* %cs_new_protected:Nn\stex_kpsewhich:Nn\group_begin:
* %catcode'\=12
* %sys_get_shell:nnnN{kpsewhich-#2}{}\l_tmpa_tl
* %t1_get_eq:NN\l_tmpa_tl\l_tmpa_tl
* %group_end:
* %exp_args:NNo\stex_set:Nn#1{\l_tmpa_tl}
* %t1_trim_spaces:N#1
* %

(_End definition for %stex_kpsewhich:Nn. This function is documented on page 13._)

\stex_get_env:Nn
* %sys_if_platform_windows:TF{
* %cs_new_protected:Nn\stex_get_env:Nn\group_begin:
* %escapechar=-1\cactcode'\=12
* %exp_args:NNe\stex_kpsewhich:Nn#1{-expand-var-\c_percent_str#2}c_percent_str}
* %exp_args:NNx\sse:nn\group_end:{
* %str_set:Nn\exp_not:N#1{#1}
* %
* %t
* %cs_new_protected:Nn\stex_get_env:Nn{
* %stex_kpsewhich:Nn#1{-var-value-#2}
* %
* %

(_End definition for %stex_get_env:Nn. This function is documented on page 13._)

#### Logging

* %(@0=stex_debug)
* %sc_new_protected:Nn\stex_debug:nn
* %exp_args:NNo\clist_if_in:NNTF\c_stex_debug_clist{\tl_to_str:n{all}}{
* %stex_debug.:nn#1}{
* %exp_args:NNo\clist_if_in:NNT\c_stex_debug_clist{\tl_to_str:n{#1}}{
* %stex_debug.:nn#1}{#2}
* %




#### Group-like Behaviours

```
<@@=stex_groups> <user_pseudogroup.nn <user_pseudogroup.restore:N
``` <exp_args:Nm>use:nn } <cs_new:Nm{stex_pseudogroup.restore:N{ <tl_if_exist:NTF#1{ <tl_set:Nm<exp_not:N#1{ <exp_args:No<exp_not:n#1} } <cs_undefine:N<exp_not:N#1 } } } ```
(End definition for _stex_pseudogroup:nn and _stex_pseudogroup_restore:N. These functions are documented on page 131_.)
``` <user_pseudogroup.with:nn ```
<cs_new_protected:Nm{stex_pseudogroup.with:nn{ <tl_map.inline:nn{#1} <cs_set.eq:cN{_stex_groups_tl_to_str:n{##1}}##1 } } #2 <tl_map.inline:nn{#1} <cs_set.eq:cN<eff#1{_stex_groups_tl_to_str:n{#1}} <cs_undefine:c{_stex_groups_tl_to_str:n{#1}} } }
``` <user_pseudogroup.with:nn. This function is documented on page 131_.) ``` <user_pseudogroup.new:Nm{stex_pseudogroup.remove:Nm{ <user_pseudogroup.restore:Nm{ <user_pseudogroup.restore:Nm{ <user_pseudogroup.remove:Nm{ <user_pseudogroup.remove:Nm{ <user_pseudogroup.remove:Nm{ <user_pseudogroup.remove:Nm{ <user_pseudogroup.remove:Nm{ <user_pseudogroup.remove:Nm{ <user_pseudogroup.remove:Nm{ <user_pseudogroup.remove:Nm{ <user_pseudogroup.remove:Nm{ <user_pseudogroup.remove:Nm{ <user_pseudogroup.remove:Nm{ <user_pseudogroup.remove:Nm{ <user_pseudogroup.remove:Nm{ <user_pseudogroup.remove:Nm{ <user_pseudogroup.remove:Nm{ <user_pseudogroup.remove:Nm{ <user_pseudogroup.remove:Nm{ <user_pseudogroup.remove:Nm{ <user_pseudogroup.remove:Nm{ <user_pseudogroup.remove:Nm{ <user_pseudogroup.remove:Nm{ <user_pseudogroup.remove:Nm{ <user_pseudogroup.remove:Nm{ <user_pseudogroup.remove:Nm{ <user_pseudogroup.remove:Nm{ <user_pseudogroup.remove:Nm{ <user_pseudogroup.remove:Nm{ <user_pseudogroup.remove:Nm{ <user_pseudogroup.remove:Nm{ <user_pseudogroup.remove:Nm{ <user_pseudogroup.remove:Nm{ <user_pseudogroup.remove:Nm{ <user_pseudogroup.remove:Nm{ <user_pseudogroup.remove:Nm{ <user_pseudogroup.remove:Nm{ <user_pseudogroup.remove:Nm{ <user_pseudogroup.remove:Nm{ <user_pseudogroup.remove:Nm{ <user_pseudogroup.remove:Nm{ <user_pseudogroup.remove:Nm{ <user_pseudogroup.remove:Nm{ <user_pseudogroup.remove:Nm{ <user_pseudogroup.remove:Nm{ <user_pseudogroup.remove:Nm{ <user_pseudogroup.remove:Nm{ <user_pseudogroup.remove:Nm{ <user_pseudogroup.remove:Nm{ <user_pseudogroup.remove:Nm{ <user_pseudogroup.remove:Nm{ <user_pseudogroup.remove:Nm{ <user_pseudogroup.remove:Nm{ <user_pseudogroup.remove:Nm{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ {<user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ {<user_pseudogroup.remove:N{ <user_pseudogroup.remove:N{ {<user_pseudogroup.remove:N{ {<user_pseudogroup.remove:N{ {<user_pseudogroup.remove:N{ {<present

















\l_stex_current_doc_uri

(_End definition for \l_stex_current_doc_uri. This variable is documented on page 128._)

\scs_set_document_uri:

\scs_new_protected:Nn \stex_set_document_uri: {

\stex_uri_from_current_file:Nn \l_stex_current_doc_uri {narr}

\stex_debug:nn(sref){Document=URI:\stex_uri_use:N \l_stex_current_doc_uri}

\scs_}

(_End definition for \stex_set_document_uri:. This function is documented on page 128._)

\scs_new_protected:Nn \stex_set_current_namespace: {

\stex_uri_from_current_file_nolang:Nn \l_stex_current_ns_uri {source-base}

\stex_debug:nn(modules){Namespace-URI:\stex_uri_use:N \l_stex_current_ns_uri}

\scs_}

(_End definition for \stex_set_current_namespace:. This function is documented on page 128._)

We determine the PWD

\scs_pred_file

\scs_train_file

\scs_get_env:Nn\l_stex_path_str{CD}

\scs_get_env:Nn\l_stex_path_str{PWD}

\scs_file_resolve:No \c_stex_pred_file \l_stex_path_str

\scs_set_eq:Nn \c_stex_main_file \c_stex_pred_file

\scs_put_right:Nx \c_stex_main_file {\jobname}tl_to_str:n{.tex}

\scs_debug:nn {files}{PWD:\stex_file_use:N \c_stex_pred_file}

(_End definition for \c_stex_pred_file and \c_stex_main_file. These variables are documented on page 127._)

#### 13.2.9 File Hooks

keeps track of file changes:

\scs_get_clear_new:Nn_stex_path_stack

\scs_clear_new:Nn \stex_filestack_push:n {

\stex_str_finds_with:nnTP {#1}{.tex}

\stex_file_resolve:No \g_stex_current_file {#1}

\stex_file_resolve:No \g_stex_current_file {#1.tex}

\stex_file_absolute:NF \g_stex_current_file {

\stex_file_resolve:Nx \g_stex_current_file {

\stex_file_use:N \c_stex_pred_file / \stex_file_use:N \g_stex_current_file












}
1516{STEXInternalSrefRestoreTarget
1517{stex_uri_use:N\l_stex_current_doc_uri}
1518{\l_stex_refs_str}
1519{\@currentcounter}
1520{\@currentlabel}
1521{\t1_if_exist:NT}@currentlabelname{
1523{exp_args:No\exp_not:n\@currentlabelname
1524}
1535{}
1536{}
1537{exp_args:Nx\label {sref@\l_stex_ref_url_str}
1538{stex_if_do_html:T {
1539}pdfdest name "sref@\l_stex_ref_url_str" xyz\relax
1530}
1531}
1532}
1533{NewDocumentCommand \sreflabel {m} {stex_ref_new_doc_target:n {#1}}
1534}
1535{cs_new_protected:Nn\__stex_refs_add_doc_ref:nn {
1536{seq_if_in:NnTF\g_stex_refs_files_seq {#1} {
1537{seq_if_in:cnF{g_stex_refs_#1_seq}{#2}}
1538{seq_gput_left:cn{g_stex_refs_#1_seq}{#2}
1539}
1540}{seq_gput_right:Nn\g_stex_refs_files_seq {#1}
1542{seq_new:c{g_stex_refs_#1_seq}
1543{seq_gput_left:cn{g_stex_refs_#1_seq}{#2}
1544}
1545{cs_generate_variant:Nn\__stex_refs_add_doc_ref:nn {xo,xx} } (_End definition for \stex_ref_new_doc_target:n and \sreflabel. These functions are documented on page 110._) }
1556} \stex_keys_define:nnnn{sref / 1}{
1548{% TODO get rid of this
1540fallback.code:n = {},
1550pre.code:n = {},
1551post.code:n = {}
1552}{archive file}
1553} \stex_keys_define:nnnn{sref / 2}{}{archive file, title}
1554}
1555{str_new:N\l\_stex_refs_default_archive_str
1556}{str_new:N\l\_stex_refs_default_file_str
1557}{tl_new:N\l\_stex_refs_default_title_tl
1558}
1559{cs_set_protected:Nn\__stex_refs_set_keys_b:n {
1560}tl_if_empty:nTF{#1}{
1561} \stex_set_eq:NN\l\_stex_key_archive_str\l\_stex_refs_default_archive_str
1562} \stex_set_eq:NN\l\_stex_key_file_str\l\_stex_refs_default_file_str
1563}{tl_set_eq:NN\l\_stex_key_title_tl\l\_stex_refs_default_title_tl
1564}}


1617 \1_stex_refs_file{narr}
1618 \str_set:Nx\l_stex_refs_uri_str{}stex_uri_use:N\l_stex_refs_uri}
1619 }
1620 \cs_new_protected:Nn\__stex_refs_find_uri_in_file:nnn{
1622 \stex_debug:nn{sref}{Checking-file-#2}
1623 \seq_map_inline:cn{g_stex_refs_#2_seq}{
1624 \str_if_eq:nnT{#1}{
1625 \str_set:Nx\l_stex_refs_uri_str{}stex_uri_use:N\l_stex_current_doc_uri}
1626 \stex_debug:nn{sref}{Found.}
1627 #3
1638 }
1639 }
1630 Doing the actual referencing:
1631 \cs_new_protected:Nn\__stex_refs_do_autoref:n{
1632 \cs_if_exist:cTF{autoref}{
1633 \exp_args:Nx\autoref{sref@#1}
1634 }{
1635 \exp_args:Nx\ref{sref@#1}
1636 }
1637 }
1638
1639 \cs_new_protected:Nn\__stex_refs_do_sref:nn{
1640 \str_if_empty:NTF\l\__stex_refs_uri_str{
1641 \str_if_empty:NTF\l\__stex_key_file_str{
1642 \stex_debug:nn{sref}{autoref-on-\tex_uri_use:N\l\_stex_current_doc_uri?#1}
1643 \exp_args:Ne\__stex_refs_do_autoref:n{}stex_uri_use:N\l\_stex_current_doc_uri?#1}
1644 }{
1645 \stex_debug:nn{sref}{srefin-on-#1}
1646 \__stex_refs_set_keys_b:n{#2}
1647 \__stex_refs_do_sref_in:n{#1}
1648 }
1649 }{
1650 \exp_args:NNo\seq_if_in:NnTF\g\__stex_refs_files_seq\l\__stex_refs_uri_str{
1651 \stex_debug:nn{sref}{Using-ref-file-\l\_stex_refs_uri_str}
1652 \exp_args:Nnx\seq_if_in:cnTF{g_stex_ref,\l\__stex_refs_uri_str_seq}{
1653 \stex_debug:nn{sref}{Reference-found-in-ref-files;autoref-on-\l\_stex_refs_uri_str?
1654 \__stex_refs_do_autoref:n{\l\__stex_refs_uri_str?#1}
1655 }{
1656 \str_if_empty:NTF\l\__stex_key_file_str{
1657 \stex_debug:nn{sref}{in-empty;-autoref-on-\l\_stex_refs_uri_str?#1}
1658 \__stex_refs_do_autoref:n{\l\__stex_refs_uri_str?#1}
1659 }{
1660 \stex_debug:nn{sref}{in-non-empty;-srefin-on-\l\_stex_refs_uri_str?#1}
1661 \__stex_refs_set_keys_b:n{#2}
1662 \__stex_refs_do_sref_in:n{#1}
1663 }
1664 }{
1665 \stex_debug:nn{sref}{No-ref-file-found-for-\l\__stex_refs_uri_str}
1667 \str_if_empty:NTF\l\__stex_key_file_str{
1668 \stex_debug:nn{sref}{in-empty;-autoref-on-\l\_stex_refs_uri_str?#1}


}{
1723}{
1724}\l_stex_refs_return_tl
1725}
1726}{
1727\exp_args:Nnno\msg_warning:nnn{stex}{warning/smsmissing}\l_stex_refs_flo_autoref:n{
1728}\str_if_empty:NFVl_stex_refs_uri_str{\l_stex_refs_uri_str?}#1
1730}
1731}
1732}
1733}
1734}
1735}
1736
1737}cs_new_protected:Nn\__stex_refs_do_return:nnnn {
1738}tl_set:Nn\l_stex_refs_return_tl {
1739}\stex_annotate:nnn{shtml:sref={W4},shtml:srefin={\l_stex_refs_file_str}}{
1740\use:c{#3autorefname}-#1{tl_if_empty:NFVl_stex_key_title_tl{
1741}{\l_if_empty:NFVl_stex_key_title_tl{
1742}{\l-in-\l_stex_key_title_tl
1743}
1744}
1745}
1746}
1747}cs_new_protected:Nn\__stex_refs_restore_target:nnnnn {
1748}str_if_empty:NFVl_stex_refs_uri_str {
1750\exp_args:No\str_if_eq:nnT\l\l_stex_refs_id_str {W2}{
1751\_stex_refs_do_return:nnnnn{W4}{#5}{#3}{#1?#2}
1752}
1753}{
1754\stex_debug:nn{sref}{\l_stex_refs_uri_str}- == - #1 -?}
1755\exp_args:No\str_if_eq:nnT\l\l_stex_refs_uri_str {#1}{
1756\stex_debug:nn{sref}{\l_stex_refs_id_str == - #2 -?}
1757\exp_args:No\str_if_eq:nnT\l\l\_stex_refs_id_str {#2}{
1758\stex_debug:nn{sref}{success!}
1759\l_stex_refs_do_return:nnnn{#4}{#5}{#3}{#1?#2}
1760\endinput
1761}
1762}
1763}
1764} ```
The actual macros:
```
176NNewDocumentCommand\sref{0{}m0{}}{
176%stex_keys_set:nn{sref/1}{#1}
177%__stex_refs_find_uri:n{#2}
178%__stex_refs_do_sref:nn{#2}{#3}
1790}
1701NewDocumentCommand\extref{0{}m=m}{
171%tex_keys_set:nn{sref/1}{#1}
1712%__stex_refs_find_uri:n{#2}
1723\_stex_refs_set_keys_b:n{#3}
1734\str_if_empty:NFVl_stex_key_file_str {
1757\msg_error:nn{stex}{error/extreffmissing}











* [226] \cs_new_protected:Nn __stex_smsmode_check_begin:Nn {
227 % \stex_debug:nn(sms){Checking-environment-#2}
228 \seq_if_in:NxTF #1 { \t1_to_str:n(#2) }{
229 \stex_debug:nn(sms){Environment-#2}
230 \begin{#2}
231 \text{} \_stex_smsmode_do:w
232 }
233 }
234 }
235 \cs_new_protected:Nn __stex_smsmode_check_end:Nn {
236 % \stex_debug:nn(sms){Checking-end-environment-#2}
237 \seq_if_in:NxTF #1 { \t1_to_str:n(#2) }{
238 \stex_debug:nn(sms){End-Environment-#2}
239 \end{#2}
2310 \text{} \stex_if_eq:nnTF(#2){document} \endinput
2311 \_stex_smsmode_do:w
232 }
233 }
234 } \

(End definition for \stex_smsmode_do: This function is documented on page 125.)

### 13.6 Modules

#### 13.6.1 The module-environment

#### 13.6.2 (@@-stex_modules)

The current module:
235 \stx_new:N \l_stex_current_module_str (End definition for \l_stex_current_module_str. This variable is documented on page 111.)

\l_stex_all_modules_seq Stores all modules currently in scope
236 \seq_new:N \l_stex_all_modules_seq (End definition for \l_stex_all_modules_seq. This variable is documented on page 111.)

\stex_every_module:n
237 \stex_every_module:n
238 \stex_every_module:n
239 \cs_new_protected:Nn \stex_every_module:n {
240 \l_gpu_right:Nn \g_stex_every_module_tl {#1 }
241 \

(End definition for \stex_every_module:n. This function is documented on page 111.)

\stex_module_setup:n Sets up a new module:
242 \cs_new_protected:Npn \stex_module_setup:n {
243 \stex_if_in_module:TF \stex_module_setup_setup_nested:n \_stex_module_setup_setup_setup:n
244 }
245 \cs_new_protected:Nn \_stex_module_setup_setup_top:n {
246 \_stex_module_setup_get_uri_str:n(#1)



){
234 }{
235 }{
236 }exp_after:wN \prop_to_keyval:N \cs:w
237 \c_stex_module_\l_stex_current_module_str _symbols_prop
238 \cs_end:
239 }{
2390 \exp_after:wN \exp_after:wN \exp_after:wN \exp_not:n
2391 \exp_after:wN \exp_after:wN \exp_after:wN
2392 { \cs:w \c_stex_module_\l_stex_current_module_str _code \cs_end: }
2393 }{
2394 \prop_map_function:cNC_stex_module_\l_stex_current_module_str _notations_prop}
2395 \_stex_modules_persist_nots_i:nn
2396 \exp_not:N \STEXRestoreNotsEnd {}
2397 }
2398 }
2400 \cs_new_protected:Nn \_stex_modules_restore_module:nnnn {
2401 \prop_gset_from_keyval:cn{c_stex_module_\tl_to_str:n{#1}_morphisms_prop}{#2}
242 \cs_set:Npn \_stex_modules_tl {#3}
243 \exp_args:Nno \prop_gset_from_keyval:cn{c_stex_module_\tl_to_str:n{#1}_symbols_prop}\_stex_prop_map_inline:cn{c_stex_module_\tl_to_str:n{#1}_symbols_prop}{
244 \stex_ref_new_symbol:n{#1}_stex_intro}
245 }
2467 \cs_gset:cpn{c_stex_module_\tl_to_str:n{#1}_code}{#4}
2480 \prop_gclear:c{c_stex_module_\tl_to_str:n{#1}_notations_prop}
2490 \str.set:Nn \_stex_modules_restore_mod_str {#1}
2401 \group_begin:
2491 \catcode^:=@\relax
2412 \catcode^:=12}relax
2413 \_stex_modules_restore_nots:n
2414 }
2415 \cs_new:Nn \_stex_modules_persist_nots_i:nn {
2417 \exp_not:n{#2}
2418 }
2419
2420 \quark_new:N \STEXRestoreNotsEnd
2421 \cs_new_protected:Nn \_stex_modules_restore_nots:n {
2423 \_stex_modules_restore_nots_i:nn
2424 }
2425 \cs_new_protected:Nn \_stex_modules_restore_nots_i:nn {
2427 \tl_if_eq:nnTF{#1}{\STEXRestoreNotsEnd}{
2428 \group_end:
2429 }{
2430 \_stex_modules_restore_nots_ii:nnnnn {#1}
2431 }
2432 }
2433
2444 \cs_new_protected:Nn \_stex_modules_restore_nots_ii:nnnnn {
2445 \cs_set:Npn \l_stex_modules_tl {{#4}{#5}}
245 \exp_args:NNeuse:nn\prop_gput:cnn{
2467 \c_stex_module_\l_stex_modules_restore_mod_str _notations_prop}

{tl_to_str:n{#1!#2}}{
2430 {tl_to_str:n{#1}}{tl_to_str:n{#2}}{#3}
2440 {exp_args:No \exp_not:n \l_stex_modules_tl
2441 }
2442 }
2443 {_stex_modules_restore_nots_i:n
2444 }

(_End definition for \stex_close_module:. This function is documented on page 111._)

\l_stex_metatheory_uri

2445 \tl_new:N \l_stex_metatheory_uri

(_End definition for \l_stex_metatheory_uri. This variable is documented on page??._)

\setmetatheory

2446 \cs_new_protected:Nn \_stex_modules_set_metatheory:nn {
2447 \group_begin:
2448 \stex_debug:nn{metatheory}{Setting-metatheory-[#1]#2}
2440 \stex_import_module_uri:nn { #1 } { #2 }
2450 \stex_debug:nn{metatheory}{Here:~J
2451 \l_stex_import_archive_str~~J
2452 \l_stex_import_path_str~~J
2453 \l_stex_import_name_str~~J
2454 \stex_import_require_module:000
2456 \l_stex_import_archive_str
2457 \l_stex_import_path_str
2458 \l_stex_import_name_str
2459 \stex_debug:nn{metatheory}{Found:~\l_stex_import_ns_str}
2460 \exp_args:Nne \see:nn {
2461 \group_end:\stex_uri_resolve:Nn \l_stex_metatheory_uri
2462 }{{\l_stex_import_ns_str}}
2463 \
2464 \newDocumentCommand \setmetatheory {O{} m}{
2466 \_stex_modules_set_metatheory:nn { #1 }{ #2 }
2467 \stex_smsmmode_do:
2468 \stex_sms_allow_escape:N \setmetatheory

(_End definition for \setmetatheory. This function is documented on page??._)

Keys and key handling:
2470 \stex_keys_define:nnnn{module}{
2471 \str_clear:N \l_stex_key_sig_str
2472 }{
2473 meta.code:n = {
2474 \str_if_empty:nTF {#1}{
2475 \tl_clear:N \l_stex_metatheory_uri
2476 }{
2477 \stex_uri_resolve:Nx \l_stex_metatheory_uri { #1 }
2478 }
2479 },
2480 ns.code:n = {




* [commandchars=

{},codes=] (_End definition for_ \stex_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_notation:mmmmn_ #1 : URI _user_module_add_notation:eeeeeo #2 : variant _user_set_notation_more:mmn #3 : arity #4 : macro body #5 : op * [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=

{},codes=] (_set_module_add_symbol:nnnnnnN. This function is documented on page 1.)

* [commandchars=





* {\_set_get_symbol_mod_str?\l_set_get_symbol_name_str}
* }
* }
* } cs_new_protected:Nn\__set_features_add_definiens:nn{
* {_stex_features_set_definiens_macros:#1\__stex_features_break:
* {_stex_assign_do:n{#2}
* #2
* } cs_new_protected:Npn\__stex_features_set_definiens_macros:#1?#2?#3\__stex_features_break:
* {_str_set:Nn\l_stex_get_symbol_mod_str{#1?#2}
* {_str_set:Nn\l_stex_get_symbol_name_str{#3}
* {_exp_args:Nne\use:nn{_stex_features_set_definiens_macros_i:nnnnnnnnn}{
* {_prop_item:Nn\l_stex_morphism_symbols_prop{[#1?#2]/[#3]}
* }
* } cs_new_protected:Nn\__stex_features_set_definiens_macros_i:nnnnnnnnn {
* {_tl_set:Nn\l_stex_get_symbol_def_tl{#4}
* } cs_new_protected:Nn\__stex_structural_feature_morphism_end:{
* {_str_gset_eq:NN\l_stex_feature_name_str\l_stex_feature_name_str
* {_str_gset_eq:NN\l_stex_current_domain_str\l_stex_current_domain_str\l_stex_current_domain_str\l_stex_current_domain_str\l_stex_morphism_symbols_prop\l_stex_morphism_symbols_prop\l_stex_morphism_remames_prop\l_stex_append\l_stex_append\l_stex_morphism_remames_prop\l_stex_get_get:NN\l_stex_morphism_membisms_seq\l_stex_morphism_ morphisms_seq\l_stex_features_do_elaboration:
* {_str_id_do_html:TF{
* {_send_state_annotate_env}
* } group_end:
* } cs_new_protected:Nn\__stex_features_setup:{
* {_prop_clear:N\l_stex_morphism_symbols_prop\l_stex_morphism_remames_prop\l_stex_append\l_stex_morphism_ morphisms_seq\l_stex_features_do_decls:
* {_exp_args:No\__stex_features_do_morphisms:n\l_stex_current_domain_str\l_stex_protected:Nn\__stex_features_rename_all:{
* } cs_new:Npn\__stex_features_clean:nnw[#1]/#2\__stex_end:{
* {_#1}/[#2]
* } cs_new_protected:Nn\__stex_features_do_decls:{
* {_exp_args:No\stex_iterate_symbols:nn\l_stex_current_domain_str\l_stex_str_if_starts_with:nnTF{#3}[{_exp_args:NNeprop_put:Nnn\l_stex_morphism_symbols_prop\l_stex_features_clean:nnw#3\__stex_end:



) } __ste_features_renamed_check:nnnnnn(#1}##1=#2
2081 } }str_if_empty:NT \l_stex_get_symbol_name_str {
2083 \msg_error:nnxx{stex}{error/unknownsymbolin}{#1}{
2084  morphism=\l_stex_feature_name_str
2085 } }
2086 } }
2088 }
2089 } }
2090 \cs_new_protected:Npn \_stex_features_renamed_check:nnnnnn #1%2?#3?#4=#5#6 {
2091 \str_if_eq:nnTF{#1}{#5}{
2092 \exp_args:Nmx use:nn{\_stex_features_check_break:nnnnnnnnnn(#2?#3}{#4}{
2093 \prop_item:Nn \l_stex_morphism_symbols_prop {[#2?#3]/[#4]}
2094 }
2095 } } } ```
Listing 1: \l_stex_features_renamed_check:nnnnnn #1%2?#3?#4=#5#6 {
2096 \prop_item:Nn \l_stex_morphism_symbols_prop {[#2?#3]/[#4]}
2090 } }
3001 } }
3002 } }
3003 } }
```

Listing 2: \l_stex_features_check:nnnn #1[#2]/[#3]#4 {
3006 \str_if_eq:nnTF{#1}{#3}{
3007 \str_if_eq:nnTF{#1}{#4}{
3008 \_stex_features_check_break:nnnnnnnn(#2}{#3}{#4}
3010 \_stex_features_check_break:nnnnnnnn(#2){#3}{#4}
3011 \{use_none:nnnnnn
3012 }
3013 }
3014 }
3015 \cs_new_protected:Nn \_stex_features_check:nnnnnnnnnnn {
3017 \prop_map_break:n{
3018 \str_set:Nn \l_stex_get_symbol_mod_str(#1}
3019 \str_set:Nn \l_stex_get_symbol_name_str(#2}
3020 \str_set:Nn \l_stex_get_symbol_macro_str(#3)
3021 \int_set:Nn \l_stex_get_symbol_arity_int {#4}
3022 \tl_set:Nn \l_stex_get_symbol_args_tl {#5}
3023 \tl_set:Nn \l_stex_get_symbol_def_tl {#6}
3024 \tl_set:Nn \l_stex_get_symbol_type_tl {#7}
3035 \tl_set:Nn \l_stex_get_symbol_return_tl {#8}
3036 \tl_set:Nn \l_stex_get_symbol_invoke_cs {#9}
3027 } }
3028 } ```

(_End definition for \stex_get_in_morphism:n. This function is documented on page 120._)





\msg_error:nnx{stex}{error/unknownmodule}{\l_stex_import_uri_str?#1}
3213}
3214}
3215
3216}cs_new_protected:Npn \_stex_importmodule_check_file:nn #1 {
3217} \stex_debug:nn{imports}{Checking- \l_stex_importmodule_str #1}
3218}lfFileExists{\l_stex_importmodule_str #1}{
3219} \stex_debug:nn{imports}{Success}
3210}str_set:Nx \l_stex_importmodule_str {\l_stex_importmodule_str #1 }
3211}
3212}
3213} \
3214} \
3215} \stex_import_require_module:nnn. This function is documented on page 119.)

\importmodule
3216} \stex_new_styablablemd:nnnn{importmodule} {Q} m } {
3217} \stex_importmodule_import_module:nn {#1}{#2}
3218} \stex_mssmode_do:
3219} \stex_deactivate_macro:Nn \importmodule {module-environments}
3210} cs_new_protected:Nn \_stex_importmodule_import_module:nn {
32118} \stex_import_require_module:000
3212} \l_stex_import_archive_str
3213} \l_stex_import_path_str
3214} \l_stex_import_name_str
3215} \stex_execute_in_module:x{
3216} \stex_activate_module:n{\l_stex_import_ns_str}
3217} \stex_module_add_morphism:nnnn
3218} \stex_import_ns_str}{import}{
3219} \stex_if_do_html:T {
3210} \stex_annotate_invisible:nn
32112} \stex_if_smsmode:F{
32123} \stex_if_smsmode:F{
3213} \group_begin:
3214} \stex_if_set:Nn \thisarchive {#1}
3215} \stex_eq:NN \thismoduleuri \l_stex_import_ns_str
3216} \stex_eq:NN \thismodulename \l_stex_import_name_str
3217} \stex_start_apply:
3218} \group_end:
3219} \stex_new_protected:Nn \_stex_importmodule_import_module_presms:nn {
3210} \stex_import_module_uri:nnn { #1}{#2}
3219} \stex_gpu_right:Nx \stex_sms_import_code {
32110} \stex_import_require_module_safe:nnn
3212} \stex_import_archive_str}
3213} \stex_import_name_str}






}

$4%str_ifempty:NF\l_stex_morphisms_newname_str{

$4%exp_after:wN\__stex_morphisms_do_parsed_newname:\l_stex_morphisms_newname_str\__st

$4%tl_ifempty:NF\l_stex_morphisms_ass_tl{

$5%exp_args:No\_stex_assign_do:n\l_stex_morphisms_ass_tl

$5%}

$5%cs_new_protected:Nn\__stex_morphisms_do_parsed_newname:{

$5%peek_charco:NTF[{

$5%_stex_morphisms_do_parsed_newname:w

$5%}{

$5%_stex_morphisms_do_parsed_newname:w []

$5%}

$5%cs_new_protected:Npn\__stex_morphisms_do_parsed_newname:w[#1]#2\__stex_morphisms_end:{

$5%_stex_renamedecl_do:nnn{#1}{#2}

$5%}

$5%stex_new_stylable_cmd:nnnn{copromod}{m0{}m=m}{

$5%stex_structural_feature_morphism:nnnnn{#1}{morphism}{#2}{#3}{,shtml:total=false}

$5%}{slist_map_function:nN{#4}\__stex_morphisms_parse_assign:n

$5%}

$5%stex_if_smsmode:F{

$5%t1.N\thiscopyname{#1}

$5%t1.set_eq:NN{thismoduleuri\l_stex_current_domain_str

$5%stex_style_apply:

$5%}

$5%stex_structural_feature_morphism_end:

$5%stex_smsmode_do:

$5%}

$5%stex_deactivate_macro:Nn\copymod{module-environments}

$5%stex_every_module:n{

$5%stex_reactive_macro:N\copymod

$5%stex_sms_allow_escape:N\copymod

$5%stex_new_stylable_cmd:nnnn{interpretmod}{m0{}m=m}{

$5%stex_structural_feature_morphism:nnnnn{#1}{morphism}{#2}{#3}{,shtml:total=true}

$5%}{slist_map_function:nN{#4}\__stex_morphisms_parse_assign:n

$5%stex_if_smsmode:F{

$5%tl_set:Nn\thiscopyname{#1}

$5%tl_set_eq:NN{thismoduleuri\l_stex_current_domain_str

$5%stex_style_apply:

$5%stex_structural_feature_morphism_check_total:

$5%stex_structural_feature_morphism_end:

$5%stex_smsmode_do:

$5%}

*%set_deactivate_macro:Nm\interpretmod{module-environments}
*%set_every_module:n{
*%set_reactivate_macro:N%interpretmod
*%set_sms_allow_escape:N%interpretmod
*%set_new_stylable_cmd:nnnn{realize}{0{}m}{
*%set_structural_feature_morphism:nnnnn{}{morphism}{#1}{#2}{,shtml:total=true}
*%set_map_function:nN{#3}\_stex_morphisms_parse_assign:n
*%set_if_smsmode:F{
*%set_set:Nm\thiscopyname{#1}
*%set_eq:NN\thismoduleuri\l_stex_current_domain_str
*%set_style_apply:
*%set_structured_feature_morphism_check_total:
*%set_structural_feature_morphism_end:
*%set_smsmode_do:
*%set_deactivate_macro:Nm\realize{module-environments}
*%set_every_module:n{
*%set_reactivate_macro:N\realize
*%set_sms_allow_escape:N\realize

### 13.8 Symbols

#### Declarations

Some setup:

*%set_if_check_terms:IF{
*%set_if_check_terms:IF{
*%set_if_hntl_backend:TF{
*%set_if_check_terms:{p,T,F,TF}{
*%set_return_false:
*%set_get_env:Nm\_stex_symdecl_env_str{STEX_CHECKTERMS}
*%set_if_empty:NFV\_stex_symdecl_env_str{
*%set_if_eq:nnF\_%set_symdecl_env_str{false}{
*%set_true:N\_%set_check_terms_bool
*%set_if:NTF\_c_stex_check_terms_bool{
*%set_if_check_terms:{p,T,F,TF}{
*%set_return_true:
*%set_if_check_terms:{p,T,F,TF}{
*%set_return_false:* [3646] } (_End definition for \stex_if_check_terms:TF. This function is documented on page 113._) \stex_check_term:n
* [3646] \cs_new_protected:Nn \stex_check_term:n {
* [3650] \hbox_set:Nn \l_tmpa_box {
* [3651] \group_begin:
* [3652] \#1$
* [3653] \group_end:
* [3654] \
* [3655] \
* [3656] \{
* [3657] \cs_new_protected:Nn \stex_check_term:n {}
* [3658] \

(_End definition for \stex_check_term:n. This function is documented on page 113._) symbolecl arguments:
* [3659] \stex_keys_define:nnnn(symargs){
* [3660] \str_clear:N \l_stex_key_args_str
* [3661] \str_clear:N \l_stex_key_role_str
* [3662] \str_clear:N \l_stex_key_reorder_str
* [3663] \str_clear:N \l_stex_key_assoc_str
* [3664] \{
* [3665] \args.str_set:N = \l_stex_key_args_str,
* [3666] \stex_set:N = \l_stex_key_reorder_str,
* [3667] \stex_key_order_str
* [3670] \str_clear:N \l_stex_key_name_str
* [3671] \stex_key_args_str
* [3672] \stex_key_define:nnnn{decl}{
* [3673] \str_clear:N \l_stex_key_name_str
* [3674] \str_clear:N \l_stex_key_args_str
* [3675] \l_clear:N \l_stex_key_type_tl
* [3676] \l_clear:N \l_stex_key_def_tl
* [3677] \l_clear:N \l_stex_key_return_tl
* [3678] \list_clear:N \l_stex_key_argtypes_clist
* [3679] \{
* [3680] name.str_set:N = \l_stex_key_name_str,
* [3681] \stex_key_return_tl,
* [3682] \stex_type.clist_set:N = \l_stex_key_arguments_tl,
* [3683] \stex_key_type_tl,
* [3684] \stex_key_def_tl,
* [3685] \stex_key_def_tl,
* [3686] \stex_def_tl,
* [3687] \stex_def_tl,
* [3688] \stex_def_tl,
* [3689] \stex_def_tl,
* [3690] \stex_def_tl,
* [3691] \stex_def_tl,
* [3692] \stex_def_tl,
* [3693] \stex_def_tl,
* [3694] \stex_def_tl,
* [3695] \stex_def_tl,
* [3696] \stex_def_tl,
* [3697] \stex_def_tl,
* [3698] \stex_def_tl,





%str_set:Nx\l_stex_key_name_str{\l_stex_key_name_str-sym}
3%%
4%str_set:Nn\l_stex_key_role_str{textsymdecl}
5%
6%
6%tex_symdecl_do:
6%tex_symdecl_check_terms:
6%exp_args:Nnx\use:nn\stex_module_add_symbol:nnnnnnnnN}{
6%
6%tex_macroname_str}
6%
6%tex_key_name_str}
6%
6%tex_symdecl_if_empty:NF\l_stex_key_def_tl{DEFED}}
6% type
6%tex_imvec:c{#name_nospace}%return
6%tex_invoke_text_symbol:
6%
6%
6%tex_grgs:Ne\stex_ref_new_symbol:n
6%
6%
6%tex_current_module_str?\l_stex_key_name_str}
6%tex_if_do_html:T{
6%tex_symdecl_html:
6%
6%tex_symdecl_html:
6%
6%
6%tex_in\l_stex_get_symbol_arity_int0
6%
6%
6%tex_key_op_tl
6%
6%tex_clear:N\l_stex_key_intent_str
6%
6%tex_clear:N\l_stex_key_prec_str
6%
6%tex_eq:NN\l_stex_get_symbol_mod_str\l_stex_current_module_str
6%
6%tex_get:NN\l_stex_get_symbol_name_str\l_stex_key_name_str
6%tex_notation_parse:n{\hbox{#3}}
6%tex_notation_add:
6%tex_in_do_html:T{
6%tex_id_comp{_comp}
6%tex_notation_do_html:n{\l_stex_get_symbol_mod_str}%
6%tex_execute_in_module:x{
6%tex_symdecl_set_textsymdecl_macro:nnn{#1}{\l_stex_current_module_str?\l_stex_key_nam}
6%tex_not:n{#3}}
6%tex_if_smsmode:F{
6%
6%tex_begin:
6%
6%tex_symdecl_set:Nx\thisedcluri{\l_stex_current_module_str?\l_stex_key_name_str}
6%
6%tex_eq:NN\thisedclname\l_stex_key_name_str}
6%tex_skip_apply:
6%
6%tex_smsmode_do:
6%tex_descuvdecl_(module-environments)
6%tex_every_module:n{\stex_reactivate_macro:N\textsymdecl}
6%tex_sms_allow_escape:N\textsymdecl
6%
6%tex_represented:Nn\_stex_symdecl_set_textsymdecl_macro:nnn{
6%tex_set_protected:cpn{#1name_nospace}{#3}

* }cs_set_protected:cpn{#name}{
* \mode_if_vertical:T{\hbox_unpack:N\c_empty_box}
* \mode_if_math:T\hbox{let\space\relax\#3}
* \mode_if_math:F{cs_if_exist:NT\xspace\xspace}
* }
* }
* }cs_new_protected:Nn \stex_invoke_text_symbol:{
* \mode_if_vertical:T{\hbox_unpack:N\c_empty_box}
* \stex_term_oms_or_ovn:nnn{}{\hbox_un_comp{let\space\relax\l_stex_current_return_tl}}
* \group_end:\mode_if_math:F{\cs_if_exist:NT\xspace\xspace}
* } (End definition for \text{textsyndecl. This function is documented on page 77.)

(\stex_get_symbol:n)

* \cs_new_protected:Nn \stex_get_symbol:n {
* \stex_get_symbol:n{#1}
* \stex_if_empty:NT \l_stex_get_symbol_name_str {
* \msg_error:nnn{stex}{error/unknownsymbol}{#1}
* }
* }
* \cs_new_protected:Nn \stex_get_symbol:n {
* \stex_clear:N \l_stex_get_symbol_mod_str
* \stex_clear:N \l_stex_get_symbol_name_str
* \cs_if_exist:CTF {#1}{
* \cs_set_eq:q:Nc \l_stex_symbolecl_cs {#1}
* \% command name
* \exp_args:Nc \l_if_empty:nTF {\cs_argument_spec:N \l_stex_symbolecl_cs }{
* \%...that takes no arguments
* \exp_args:Nc \cs_if_eq:NTF {\t\l_head:N \l_stex_symbolecl_cs}
* \stex_invoke_symbol:nnnnnnnNN
* \stex_symbolecl_get_symbol_from_cs:
* \(\l_stex_symbolecl_get_symbol_from_string:n {#1}
* \stex_symbolecl_get_symbol_from_string:n {#1}
* \stex_symbolecl_get_symbol_from_string:n {#1}
* \stex_symbolecl_get_symbol_from_string:n {#1}
* \stex_symbolecl_get_symbol_from_string:n {#1}
* \stex_symbolecl_get_symbol_from_string:n {#1}
* \stex_symbolecl_get_symbol_from_string:n {#1}
* \stex_symbolecl_get_symbol_arity_int
* \stex_symbolecl_get_symbol_from_cs:{
* \stex_debug:nnn{symbols}{Gatting-from-cs...}
* \stex_pseudogroupwith:nn{\stex_invoke_symbol:nnnnnnnnN}{
* \cs_set:Npn \stex_invoke_symbol:nnnnnnnnN ##1 ##2 ##3 ##4 ##5 ##6 ##7 ##8 {
* \stex_set:Nn \l_stex_get_symbol_mod_str {##1}
* \stex_set:Nn \l_stex_get_symbol_name_str {##2}
* \int_set:Nn \l_stex_get_symbol_args_tl {##4}
* \stex_set:Nn \l_stex_get_symbol_def_tl {##5}
* \stex_set:Nn \l_stex_get_symbol_type_tl {##6}



___stex_notations_map_args_ii:w#1#6____stex_notations_args_end:
400 }
4100 } (_End definition for_tex_map_args:N and_tex_map_notation_args:N. These functions are documented on page??.) notation arguments:
4101 \stex_keys_define:nnnm{notation}{
4102 \str_clear:N\l_stex_key_variant_str
4103 \str_clear:N\l_stex_key_prec_str
4104 \str_clear:N\l_stex_key_op_tl
4105 \str_clear:N\l_stex_key_intent_str
4106 \clist_clear:N\l_stex_key_intent_args_clist
4107 }{
4108 variant.str_set_x:N=\l_stex_key_variant_str,
4109 prec.str_set_x:N=\l_stex_key_prec_str,
4110 op.tl_set:N=\l_stex_key_op_tl,
4111 intent.str_set:N=\l_stex_key_intent_str,
4112 argnames.clist_set:N=\l_stex_key_intent_args_clist,
4113 unknown.code:n={
4114 \str_set_eq:NN\l_stex_key_variant_str\l_keys_key_str
4115 }
4116 }{style}

notation
4117 \stex_new_stylable_cmd:nnnm{notation}{s=0{}m}{
4118 \stex_keys_set:nn{notation}{#3}
4119 \stex_get_symbol:n{#2}
4120 \stex_notation_parse:n{#4}
4121 \stex_if_check_terms:T{\_tex_notation_check:}
4122 \stex_notation_add:
4123 \stex_if_do_html:T{
4124 \def\comp{\_comp}
4125 \stex_notation_do_html:n{\l_stex_get_symbol_mod_str?\l_stex_get_symbol_name_str}
4126 }
4127 \IfBooleanTF#1{
4128 \stex_notation_set_default:n{
4129 \l_stex_get_symbol_mod_str?\l_stex_get_symbol_name_str
4130 }
4131 \stex_if_smsmode:F{
4133 \group_begin:
4134 \stex_notations_styledefs:
4135 \stex_style_apply:
4136 \group_end:
4137 \stex_smsmode_do:
4139 }{
4140 \cs_new_protected:Nn\__stex_notations_styledefs:{
4142 \str_set_eq:NN\thistnotationvariant\l_stex_key_variant_str
4143 \str_set:Nn\thistdeclname\l_stex_get_symbol_name_str
4144 \tl_set:Nx\thistDecluri{\l_stex_get_symbol_mod_str?\l_stex_get_symbol_name_str}
4145 \def\thistnotation





* 4358 }}
* 4356 \cs_new:Nn \_stex_notations_make_arg_html:nn {
* 4357 % \str_case:nnF #2 {
* 4358 %  a {
* 4359 % \stex_annotate:nn{shtml:argnum=#1a}{x},
* 4360 % \stex_annotate:nn{shtml:argnum=#1b}{x}
* 4361 % }}
* 4362 % B {
* 4363 % \stex_annotate:nn{shtml:argnum=#1a}{x},
* 4364 % }}
* 4365 % }{
* 4367 {
* 4368 \stex_annotate:nn{shtml:argnum=#1}{x}
* 4369 }
* 4360 % }
* 4371 }
* 4372 \cs_new:Nn \_stex_notation_make_args: {
* 4374 \_stex_map_notation_args:N \_stex_notations_make_arg:nnnnn
* 4375 }
* 4376 \cs_new:Nn \_stex_notations_make_arg:nnnnn {
* 4370 \str_case:nnF #2 {
* 4380 \stex_annotate:subscript_token{#1,1},
* 4381 \stex_annotate:subscript_token{#1,2}
* 4382 \stex_annotate:subscript_token{#1,2}
* 4383 \stex_term_arg:nnnnn{#1}{#2}{#3}{#4}
* 4390 {{#2}}{#2}{#1}{#2}{#3}{#4}
* 4391 \stex_atomate:subscript_token{#1}}
* 4392 }
* 4392 } (End definition for \_stex_notation_check: and others. These functions are documented on page??.)

\stectnotation \stex_notation set_default:n 4393 \cs_new_protected:Npn \stnotation #1 #2 {
* 4394 \stex_get_symbol:n{#1}
* 4395 \cs_if_exist:CTF{1_stex_notation_
* 4396 \l_stex_get_symbol_mod_str?\l_stex_get_symbol_name_str
* 4397 \#2_cs
* 4398 \tl_stex_eq:Nc \l_stex_notation_macrocode_cs {1_stex_notation_
* 4400 \l_stex_get_symbol_mod_str?\l_stex_get_symbol_name_str
* 4401 \#2_cs
* 4402 }


}

\stex_keys_define:nnnn{symbolef}{}{decl,notation}

\stex_key_protected:Nm_\_stex_symbolef_styledefs:{

\tl_set:Nx\thisedcluri{}{\_stex_current_module_str}%\_stex_key_name_str}

\tl_set_eq:NN{thisedclname}%_stex_key_name_str}

\tl_set_eq:NN{thirstype}%_stex_key_type_tl}

\tl_set_eq:NN{thisedfiniens}%_stex_key_def_tl}

\tl_set_eq:NN{thissargs}%_stex_key_args_str}

\tl_clear:N{thissstyle

\stex_set_eq:NN{thissnotationvariant}%_stex_key_variant_str}

\def{thissutation}

\stlevel\_stex_current_symbolstr{thisedcluri}

\def{\_comp{\_comp}}exp_args:Nme\use:nn{\_list_stex_notation_macrocode_cs}{

\stex_notation_make_args:

\$}

\stex_notation}

\stex_new_stytable_cmd:nnnn {symbolef}{ m0{}m}{

\stex_keys_set:nn{symbolef}{#2}

\stex_set:Nx\_l_stex_macroname_str{#1}

\stex_symdecl_top:n{#1}

\stex_debug:nm{symbolef}{Doing~\_l_stex_current_module_str}%\_l_stex_key_name_str}

\stex_set_eq:NN\_l_stex_get_symbol_mod_str}%\_stex_current_module_str}

\stex_eq:NN{ll_stex_get_symbol_name_str}%\_stex_key_name_str}

\stex_notation_parse:n{#3}

\stex_debug:nm{Here}{meaning\_l_stex_notation_args_tl}

\stex_notation_check:

\stex_notation_add:

\stex_if_do_html:T{

\stex_notation_do_html:n{\_stex_get_symbol_mod_str}%\_stex_get_symbol_name_str}

\stex_if_smsmmode:F{

\stex_if_smsmmode:F{

\stex_group_begin:

\stex_symdef_styledefs:

\stex_style_apply:

\stex_symdecl:N{symbolef}

\stex_symdecl:N{symbolef}

\stex_of_default_notation:p:

\stex_default_notation:p:

\stex_default_notation:p:

\stex_default_function:N{

\stex_default_notation:p:

\stex_default_function:N{

\stex_default_function:N{

\stex_do_default_notation:p:

\stex_if_empty:NTF\l_stex_current_args_tl}





\int_compare:nNnT\l_tmpa_int>\l\_stex_notations_clist_count_int{
4700 \int_set:Nn\l_tmpa_int1
4701 }
4702 \tl_put_right:Nx\l_tmpa_tl{
4703 \exp_after:wN\exp_not:n\exp_after:wN{\_stex_notations_map_cs:{###1}}
4704 \list_item:nn(#4)\l_tmpa_int
4705 }
4706 \seq_set_eq:NN\l_stex_aB_args_seq\l_tmpa_seq
4708 \begin{array}{#2}
4709 \l_tmpa_tl
4710 \end{array}
4711 \end{array}
4712 #1
4713 }
4714 }

(_End definition for_ \argarraymap. This function is documented on page 8.)_

#### Variables

``` \t1_new:N\l_stex_variables_prop \bool_new:N\l_stex_vars_bind_bool \cs_new_protected:Nn\_stex_variable:nnnnnnnnN{} \stex_keys_define:nnnnn{vardef}{
4720 \bool_set_false:N\l_stex_vars_bind_bool
4721 }{
4722 bind.bool_set:N=\l_stex_vars_bind_bool
4723 }{symdef}
4724 \stex_new_stylable_cmd:nnnnn{vardef}{ m0{} m} {
4726 \stex_keys_set:nn{vardef}{#2}
4727 \stex:Nx\l_stex_macroname_str{#1}
4728 \stex_if_empty:NT\l_stex_key_name_str{
4729 \strset:Nx\l_stex_key_name_str{#1}
4730 }
4731 \stex_symdecl_do:
4732 \stex_symdecl_check_terms:
4734 \_stex_vars_add:
4735 \stex_vars_macro:
4736 \stex_if_do_html:T\_stex_vars_html:
4737 \stex_set:Nn\l_stex_get_symbol_arity_int{\l_stex_get_symbol_arity_int}
4738 \stex_debug:nn{vardef}{Doing-\l_stex_key_name_str}
4740 \t1_set_eq:NN\l_stex_get_symbol_return_tl\l_stex_key_return_tl
4741 \stex_notation_parse:n{#3}
4742 \stex_if_check_terms:T{\_stex_notation_check:}
4743 \stex_vardecl_notation_macro:
4744 \stex_if_do_html:T{
4745 \def\comp{\_varcomp}
4746 \stex_notation_do_html:n\l_stex_key_name_str} } {group_begin: {tl_set_eq:NN {thisvarname \l_stex_key_name_str } {tl_clear:N {thisstyle } {str_set_eq:NN{thisnotationvariant}l_stex_key_variant_str } {def\thisnotation{ } {\let\l_stex_current_symbol_str}thisvarname } {def\compt{\_varcomp}\exp_args:Nne {\l_stex_notation_macrocode_cs{}}{ }_stex_notation_make_args: }$ } } {stex_style_apply: {group_end:\ignorespaces }{} } } {\cs_new_protected:Nn \_stex_vars_add: { \exp_args:NNN0 \exp_args:NNnx }prop_put:Nnn \l_stex_variables_prop \l_stex_key_name_str { {\l_stex_macroname_str} {\l_stex_key_name_str} {\int_use:N \l_stex_get_symbol_arity_int} {\l_stex_get_symbol_args_tl} {\exp_args:No \exp_not:n \l_stex_key_def_tl} {\exp_args:No \exp_not:n \l_stex_key_type_tl} {\exp_args:No \exp_not:n \l_stex_key_return_tl} } } } } } {\cs_new_protected:Nn \_stex_vars_macro: { \tl_set:cx{\l_stex_macroname_str}{ \-stex_invoke_variable:nnnnnnnN {\l_stex_key_name_str} {\int_use:N \l_stex_get_symbol_arity_int} {\l_stex_get_symbol_args_tl} {\exp_args:No \exp_not:n \l_stex_key_def_tl} {\exp_args:No \exp_not:n \l_stex_key_type_tl} {\exp_args:No \exp_not:n \l_stex_key_return_tl} } } } } } } } {\cs_new_protected:Nn \_stex_vars_html: { \stex_if_do_html:T { \hbox\bgroup\exp_args:Ne \stex_annotate_invisible:nn { \httml:vardef = {\l_stex_key_name_str}, \httml:args = {\l_stex_key_args_str} \htt_if_empty:NF \l_stex_macroname_str {, \httml:macroname={\l_stex_macroname_str} } } } {str_if_empty:NF \l_stex_key_assoc_str {, \httml:assoctype={\l_stex_key_assoc_str} } } } } {str_if_empty:NF \l_stex_key_role_str {, \httml:vardef = {\l_stex_key_name_str} } } } {str_if_empty:NF \l_stex_key_name_str} } } } {str_if_empty:NF \l_stex_key_name_str} } } } {str_if_empty:NF \l_stex_key_name_str} } } } {str_if_empty:NF \l_stex_key_name_str} } } } {str_if_empty:NF \l_stex_key_name_str}












* [335] \meaning\l_stex_expr_return_this_tl^J
* [336] \exp_args:No \exp_not:n \l_stex_expr_return_args_tl^^J
* [337] \exp_args:Nnx \use:nn {
* [338] \exp_after:wN \group_end: \_stex_expr_ret_cs
* [339] \{
* [339] \exp_args:No \exp_not:n \l_stex_expr_return_args_tl
* [339] \exp_args:No \exp_not:n \l_stex_expr_return_this_tl
* [339] \group_end:
* [339] \
* [339] \
* [339] \cs_new_protected:Nn \_stex_expr_return_notation:n {
* [339] \tl_if_empty:NTF \l_stex_return_notation_tl { #1 }{
* [339] \l_stex_return_notation_tl
* [339] \
* [339] \
* [339]

Custom Notations:

* [340] \scs_new_protected:Nn \_stex_expr_invoke_op_custom:n {
* [341] \stex_debug:nn{expressions}{custom-op}
* [342] \bool_set_true:N \l_stex_allow_semantic_bool
* [343] \_stex_term_oms_or_onv:nnn{}{\maincomp{#1}}
* [344] \group_end:
* [345] \
* [346] \int_new:N \l_stex_expr_arg_counter_int
* [347] \ints_geor_protected:Nn \_stex_expr_invoke_custom:n {
* [348] \stex_debug:nn{custom-notation-for-\l_stex_current_symbol_str}
* [349] \stex_pseudogroup:nn{
* [340] \bool_set_true:N \l_stex_allow_semantic_bool
* [341] \prop_geclear:N \l_stex_expr_customs_prop
* [342] \seq_gear:N \l_stex_expr_customs_seq
* [343] \int_geor:N \l_stex_expr_arg_counter_int
* [344] \tl_if_empty:NF \l_stex_current_args_tl {
* [345] \exp_after:wN \_stex_expr_add_prop_arg:nnw \l_stex_current_args_tl \_stex_args_end:
* [346] \cs_set_eq:NN \arg \_stex_expr_arg:n
* [347] \scs_set_eq:NN \l_stex_get_symbol_args_tl \l_stex_current_args_tl
* [348] \_stex_eq:NN \_stex_expr_do_ab_next:nnn \_stex_term_oma:nnn
* [349] \_stex_expr_do_ab_next:nnn{}{#1}
* [340] \{
* [341] \prop_if_exist:NT \l_stex_expr_customs_prop {
* [342] \prop_gset_from_keyval:N \exp_not:N \l_stex_expr_customs_prop {
* [343] \prop_to_keyval:N \l_stex_expr_customs_prop
* [344] \
* [345] \
* [346] \int_gset:Nn \l_stex_expr_arg_counter_int { uint_use:N \l_stex_expr_arg_counter_int}
* [347] \seq_if_exist:NT \l_stex_expr_customs_seq {




}
630 \_stex_expr_gobble:nnnnnnnn#1{\_stex_expr_end:
640 }{ _stex_expr_is_seqmap:nTF{#1}{
642 \exp_args:NNe{use:nn}\_stex_expr_do_seqmap:nnnnnn#1}
643 }{
644 \_stex_expr_aB_simple_arg:nnnnn#1}
645 }
646 }
647 }
648
649 \cs_new:Npn\_stex_expr_gobble:nnnnnnnn#1#2#3#4#5#6#7#8#9\_stex_expr_end:{
650 {#2}#3{#6}
651 }
652 }
653 \cs_new_protected:Nn\_stex_expr_aB_simple_arg:nnnnn{
654 \seq_put_right:Nx\_stex_aB_args_seq {
655 \_stex_term_arg:nnnnnn#2\int_use:N\l_stex_expr_count_int}{#3}{#4}{#5}{
656 \exp_not:n{
657 \tl_set_eq:NN\_stex_term_do_aB_clist:\_stex_expr_do_aB_clist:
658 #1 }
659 }
660 }
661 }
662 }
663 }
664 \cs_new_protected:Nn\_stex_is_sequentialized:n{
665 \group_begin:#1\group_end:
666 }
666 } ```

Conditionsals: Is the argument a sequence variable or a \seqmap?
667 \prg_new_conditional:Nnn\_stex_expr_is_varseq:n{TF}{
668 \int_compare:nNnTF{\tl_count:n{#1}}=1{
669 \exp_args:Ne\cs_if_eq:NNTF{\exp_args:No\tl_head:n{#1}}
670 \_stex_invoke_variable:nnnnnnnN{
671 \exp_args:Ne\cs_if_eq:NNTF{\exp_args:No\tl_item:nn{#1}{8}}
672 \stex_invoke_sequence:
673 \prg_return_true:\prg_return_false:
674 \prg_return_false:
675 }prg_return_false:
676 }
677 \prg_new_conditional:Nnn\_stex_expr_is_seqmap:n{TF}{
678 \int_compare:nNnTF{\tl_count:n{#1}}=3{
679 \exp_args:Ne\tl_if_eq:nnTF{\tl_head:n{#1}}{\seqmap}
681 \prg_return_true:\prg_return_false:
682 }prg_return_false:
683 }
684 % 1: name 2: arity 3: clist 4: argnum 5: argmode 6: precedence 7: argname
685 \cs_new_protected:Nn\_stex_expr_assoc_seq:nnnnnnn{
686 \group_begin:
687 \seq_clear:N\l_stex_aB_args_seq
688 \_stex_expr_assoc_make_seq:nnn{#1}{#3}{#2}

* % #1: name, #2: clist, #3:arity
* %cs_new_protected:Nn \_star_expr_assoc_make_seq:nnn {
* %cs_if_exist:cTF(1_stex_notation_#1_cs){
* %cs_set_eq:Nc \1_star_expr_cs {1_stex_notation_#1_cs}
* %cs_set_eq:Nc \1_stex_expr_cs \1_stex_default_notation
* %cs_set_eq:Nc \1_stex_expr_cs \1_stex_default_notation
* %cs_map_inline:nnn{#2}{
* %tl_if_eq:nnTF{#1}{millipes}{
* %seq_put_right:Nn \1_stex_aB_args_seq { ##1 }
* %t_compare:nNnTF{#3}=1{
* %tl_set:Nn \1_stex_expr_iarg_tl {{##1} }
* %t_set:Nn \1_stex_expr_iarg_tl {##1}
* %seq_put_right:Nx \1_stex_aB_args_seq {
* %group_begin:
* %exp_not:n {
* %tl_set_eq:NN \_stex_term_do_aB_clist: \_stex_expr_do_aB_clist:
* %def\comp{\_varcomp}
* %str_set:Nn \1_stex_current_symbol_str{#1}
* %ep_after:wN \exp_after:wN \exp_after:wN \exp_not:n
* %exp_after:wN \1_stex_expr_cs \exp_after:wN \group_end: \1_stex_expr_iarg_tl










this.tl_set:N=\l_stex_current_this_tl,
674unknown.code:n={
675}str_set_eq:NN\l_stex_structures_name_str\lkeys_key_str
676}
677}{
678
679}cs_new_protected:Nn\_stex_structures_begin:nnn{
680}stex_keys_set:nn{mathstructure}{#2}
681}str_if_empty:NT\l_stex_structures_name_str{
682}str_set:Nn\l_stex_structures_name_str{#1}
683}
684}def\comp{\_comp}
685
686}exp_args:Nne\use:nn{\stex_module_add_symbol:nnnnnnnnN}
687{{#1}{\l_stex_structures_name_str}{0}{\l_stex_current_module_str/\l_stex_structures_name_str-module
689}}
680{\stex_invoke_structure:
681}str_set:Nx\l_stex_macroname_str{#1}
682}stex_execute_in_module:x{
683}seq_clear:c{\l_stex_structure_macros_\l_stex_current_module_str/\l_stex_structures_ns
684}seq_put_right:cn{\stex_structure_macros_\l_stex_current_module_str/\l_stex_structure
685}
686}
687exp_args:No\stex_structural_feature_module:nn
688{\l_stex_structures_name_str}{structure}
688}
689}
690}
6910}
692}
693}
694}stex_sms_allow_env:n{mathstructure}
695}stex_deactivate_macro:Nn\mathstructure{module-environments}
696}stex_every_module:n{\stex_reactive_macro:N\mathstructure}
697}
698}
699}
690}cs_new_protected:Nn\_stex_structures_do_externals:{
6910}tl_set:Nn\l_stex_structures_replace_this_tl{###1}
692}exp_args:No\stex_iterate_symbols:nn\(\l\_stex_last_feature_str){
693}__stex_structures_external_decl:nnnnn{##5}{##4}{##3}{##8}
694}
695}
696}
697}
698}
699}
699}
6911}cs_new_protected:Nn\_stex_structures_external_decl:nnnnn{
692%ster_debug:nn{structure}{
693%Generating-external-declaration-\l\_stex_structures_name_str/#3-in-
694%\l\_stex_current_module_str^^J}
695%\tl_to_str:n{#1}^^J\tl_to_str:n{#2}^^J\tl_to_str:n{#4}
696%\}
697}%tl_set:Nn\l\_stex_get_symbol_args_tl{#1}
698%exp_args:Nnx\use:nn{\stex_module_add_symbol:nnnnnnnnN}{
699%\{\l_stex_structures_name_str/#3}{\int_eval:n{#2 + 1}}
690%\ti{\l\_ifempty:nF{#1}{\_stex_map_args:N\_stex_structures_shift_argls:nn}}
691%\def\{typed}
692%\{#4}stex_invoke_outer_field:
693}
693}
694}cs_new:Nn\_stex_structures_shift_argls:nnn{
695}int_eval:n{#1+1}#2









%tl_put_right:Nn %l_stex_current_redo_tl {
64% %tl_clear:N %l_stex_structures_this_tl
64% %l
64% }{
650 %tl_set:Nx %l_stex_structures_this_tl {{
651 %bool_set_true:N %l_stex_allow_semantic_bool
652 %tl_set:Nn %exp_not:N %this {
653 %exp_args:No %exp_not:n %this
654 }
655 %exp_not:n{#1}
656 %tl_set_eq:NN %this %l_stex_structures_this_tl
657 %l_stex_return_notation_tl
658 }
659 }
650 }cs_new_protected:Nn %_stex_structures_get_field_name:n {
653 %str_set:Nx %l_stex_structures_field_name_str {
654 %exp_args:Nne %exp_after:wN %use_i:nn %use:n}
655 %prop_item:Nn %l_stex_structures_prop {#1}
656 }str_if_empty:NT %l_stex_structures_field_name_str {
657 %str_set:Nn %l_stex_structures_field_name_str {#1}
658 }
659 }
651
652 }cs_new_protected:Nn %_stex_structures_invoke_field:n {
653 %prop_if_in:NnTF %l_stex_structures_prop {#1}{
654 %tex_structures_get_field_name:n{#1}
655 %tl_clear:N %l_stex_structures_more_nextsymbol_tl
656 %exp_args:NNe %seq_if_in:NnTF %l_stex_structures_assigned_seq {{tl_to_str:n{#1}}{
657 %tl_set:Nx %l_stex_structures_more_nextsymbol_tl {
658 %tl_set:Nn %exp_not:N %l_stex_structures_this_tl {
659 %exp_args:No %exp_not:n %l_stex_structures_this_tl
660 }
651 %exp_not:n %l_stex_structures_this_tl
652 %l_stex_get:NN %this %l_stex_structures_this_tl
653 }
654 %tl_set:Nn %exp_not:N %l_stex_return_notation_tl {
655 %exp_args:No %exp_not:n %l_stex_return_notation_tl
656 }
657 %exp_args:No %exp_not:n %l_stex_structures_set_comp_tl
658 }
659 %l_stex_next_symbol:n {
6662 %exp_args:No %exp_not:n %l_stex_structures_redo_tl
663 %tl_set:Nn %exp_not:N %l_stex_current_term_tl {
664 %symuse{Metatheory?record-field}{
665 %symuse{Metatheory?of-type}{
666 %exp_args:No %exp_not:n %l_stex_structures_this_tl
667 }{ %_stex_structures_current_type: }
678 }{
670 %tex_annotate:nm{shtml:term=OML,shtml:head={}l_stex_structures_field_name_str}



\cs_if_exist:cF[1_stex_notation_##1_##2_cs}{
6700 \tl_set:cn{l_stex_notation_##1_##2_cs}{
6710 } \cs_if_exist:cF[1_stex_notation_##1_cs}{
6712 \tl_set:cn{l_stex_notation_##1_cs}{
6713 } \tl_if_empty:nF{##5}{
6715 \tl_put_right:Nn \l_stex_structures_redo_tl {
6716 \cs_if_exist:cF[1_stex_notation_##1_op_##2_cs}{
6717 \tl_set:cn{l_stex_notation_##1_op_##2_cs}{
6718 } \cs_if_exist:cF[1_stex_notation_##1_op_cs}{
6720 \tl_set:cn{l_stex_notation_##1_op_cs}{##5}
672 } \cs_if_exist:cF[1_stex_notation_##1_op_##2_cs}{
6724 \tl_set:cn{l_stex_notation_##1_op_##2_cs}{
6725 \cs_if_exist:cF[1_stex_notation_##1_op__##2_cs}{
6726 \cs_if_exist:cF[1_stex_notation_##1_op__cs}{
6727 \tl_set:cn{l_stex_notation_##1_op_cs}{
6728 } \cs_if_exist:cF[1_stex_notation_##1_op_cs}{
6729 \} \cs_if_exist:cF[1_stex_notation_##1_op_cs}{
6730 \cs_if_exist:cF[1_stex_notation_##1_op_ss]{
6731 \cs_new_protected:Npn \userstructure#1 {
6734 \stex_get_mathstructure:n{#1}
6735 \seq_clear:N \l_stex_structures_imports_seq
6736 \list_map_inline:Nn \l_stex_get_symbol_type_tl {
6737 \exp_args:Ne \stex_if_module_exists:nT{\tl_to_str:n{##1}}{
6738 \seq_put_right:Nn \l_stex_structures_imports_seq{#1}
6739 }
6740 \seq_map_inline:Nn \l_stex_structures_imports_seq {
6742 \stex_if_do_html:T {
6743 \hbox{\stex_annotate_invisible:nn
6744 \hstm:\usermodule=##1}{}
6745 \stex_activate_module:n {##1}
6746 \
6747 \
6748 \

(_End definition for \userstructure. This function is documented on page 85._)

### Statements

6749 (@@=stex_statements)
6750
6751 \stex_keys_define:nnnn{statement}{
6752 \str_clear:N \l_stex_key_name_str
6753 \str_clear:N \l_stex_key_macroname_str\list_clear:N \list_key_for_clist
675 \str_clear:N \list_key_args_str
6756 \tl_clear:N \list_key_type_tl
6757 \tl_clear:N \list_key_def_tl
6758 \tl_clear:N \list_key_return_tl
6759 \list_clear:N \list_key_arguments_list
6760 \{
6761 name.str_set:N = \list_key_name_str,
6762 for.clist_set:N = \list_key_key_for_clist,
6763 macro.str_set:N = \list_key_macroname_str,
6764 % start.str_set:N = \list_key_title_str, % TODO remove
6765 type.tl_set:N = \list_key_type_tl,
6766 judgment.code:n = {},
6767 from.code:n= {}, % TODO remove
6768 to.code:n={} % TODO remove
6769 \id,title,style,symargs}

\stex_new_statement:nn
6770 \cs_new_protected:Npn \_stex_do_for_list: {
6771 \seq_clear:N \list_stex_fors_seq
6772 \list_map_inline:Nn \list_key_for_clist {
6773 \exp_args:N\stex_get_symbol:n{\tl_to_str:n{##1}}
674 \seq_put_right:Nx \list_stex_fors_seq
6775 \list_get_symbol_mod_str? \list_stex_get_symbol_name_str
6776 \
6777 \
6778
679 \cs_new_protected:Nn \_stex_statements_setup:nn {
6780 \str_if_empty:NF \list_key_macroname_str {
6781 \str_empty:NT \list_key_name_str {
6782 \str_set_eq:NN \list_key_name_str \l_stex_key_macroname_str
6783 \
6784 \
6785 \stex_do_for_list:
6786 \str_if_empty:NF \list_stex_key_name_str {
6787 \_stex_statements_force_id:
6788 \seq_put_right:Nx \list_stex_fors_seq {
6789 \l_stex_current_module_str? \l_stex_key_name_str
680 \str_set_eq:NN \list_stex_macroname_str \l_stex_key_macroname_str
6810 \str_set:Nn \list_stex_key_role_str {##2}
682 \stex_symdecl_do:
6834 \exp_args:Nnx \use:nn \stex_module_add_symbol:nnnnnnnnN}{
685 \l_stex_key_macroname_str}{\l_stex_key_name_str}
686 \int_use:N \list_stex_get_symbol_arity_int}
687 \l_stex_get_symbol_args_tl}
6878 \stex_invoke_symbol:
6890 \stex_if_do_html:T \stex_symdecl_html:
6801 \str_clear:N \list_stex_statements_uri_str
6803 \str_if_empty:NTF \list_key_name_str {
6804 \stex_debug:nn{statement}{no-name}
6805 \int_compare:nNnTF {\seq_count:N \l_stex_fors_seq} = 1 {







* [7110]{
* [7111] \int_incr:N \l_tmpa_int
* [7112] }
* [7113] \int_compare:nNnf Vl_tmpa_int = 1 {
* [7114] \int_decr:N \l_tmpa_int
* [7115] }
* [7116] \intarray_gset:Nnn \l_stex_proof_counter_intarray \l_tmpa_int {
* [7117] \intarray_item:N \l_stex_proof_counter_intarray \l_tmpa_int + 1
* [7118] }
* [7119] }
* [7120] \cs_new_protected:Npn \_stex_proof_add_counter: {
* [7121] \int_set:Nn \l_tmpa_int {1}
* [7122] \bool_while_do:nn {
* [7124] \int_compare_p:nNn {
* [7125] \intarray_item:Nn \l_stex_proof_counter_intarray \l_tmpa_int { 1}
* [7126] \}
* [7127] \cs_new_protected:Npn \_stex_proof_remove_counter: {
* [7128] \int_set:Nn \l_tmpa_int {1}
* [7129] \bool_while_do:nn {
* [7130] \intarray_gset:Nnn \l_stex_proof_counter_intarray \l_tmpa_int
* [7131] \}
* [7132] \cs_new_protected:Npn \_stex_proof_remove_counter: {
* [7133] \int_set:Nn \l_tmpa_int {1}
* [7134] \bool_while_do:nn {
* [7135] \intarray_item:Nn \l_stex_proof_counter_intarray \l_tmpa_int { 0}
* [7136] \} > 0
* [7137] \int_incr:N \l_tmpa_int
* [7138] \intarray_gset:Nnn \l_stex_proof_counter_intarray \l_tmpa_int { 0}
* [7139] \int_incr:N \l_tmpa_int
* [7140] \int_decr:N \l_tmpa_int
* [7141] \intarray_gset:Nnn \l_stex_proof_counter_intarray \l_tmpa_int { 0}
* [7142] \

spfsketch
* [7143] \newenvironment{spfsketchenv}{}{}
* [7144] \stex_new_stylable_cmd:nnnnn{spfsketch}{0{} m}{}{}
* [7145] \begin{spfsketchenv}
* [7146] \stex_keys_set:nnn{spf}{#1}
* [7147] \stex_do_for_list:
* [7148] \stex_do_id:
* [7149] \exp_args:Ne \stex_annotate:nn{
* [7140] \sthell:proofsketch={
* [7141] \seq_if_empty:NF \l_stex_fors_seq {
* [7142] \seq_use:Nn \l_stex_fors_seq,
* [7143] \
* [7144] \
* [7145] \}
* [7146] \stex_style_apply:
* [7147] \stex_tmpa_int
* [7148] \end{spfsketchenv}
* [7149] \stex_tmpa_int
* [714] \stex_tmpa_int
* 165 } \nondent\emph{spfsketchenvautorefname :}-
* 166 } (_End definition for spfsketch. This function is documented on page??._)

\spproofend This macro places a little box at the end of the line if there is space, or at the end of the next line if there isn't
* 165 \tl_set:Nn \_stex_proof_proof_box_tl {
* 166 \ltx@ifpackageloaded{amssymb}{$square$}{
* 167 \nbox{\rrule}vbox{\hrule width 6 pt\rskip 6pt\hrule}vrule}
* 168 }
* 169 }
* 170
* 171 \tl_set:Nn \spproofend {
* 172 \tl_if_empty:NF \l_stex_key_proofend_tl {
* 173 \nfill\null\n0break\hfill\l_stex_key_proofend_tl\par\smallskip
* 174 }
* 175 } (_End definition for \spproofend. This function is documented on page??._)

\stexcommentfont
* 176 \cs_new_protected:Npn \stexcommentfont {
* 177 \small\itshape
* 178 } (_End definition for \stexcommentfont. This function is documented on page??._)

\stproof (_env._)

\cs_new_protected:Nn \_stex_proof_start_list:n {
* 1780 \beginlist}{
* 1781 \setlength\topsep{Opt}
* 1782 \setlength\parset{Opt}
* 1783 \setlength\rightmargin{Opt}
* 1784 }item{#1}
* 1785 }
* 1786 \cs_new_protected:Nn \_stex_proof_end_list: {
* 1787 \end{list}
* 1788 }
* 1789
* 1790 \cs_new_protected:Nn \_stex_proof_html: {
* 1791 \stex_annotate_invisible:n{\nbox{
* 1792 \tl_if_empty:NF \l_stex_key_term_tl {
* 1793 \stex_annotate:nn{shtml:proofterm={}}}{\l_stex_key_term_tl}$
* 1794 }
* 1795 \tl_if_empty:NF \l_stex_key_method_tl {
* 1796 \stex_annotate:nn{shtml:proofmethod={}}{\l_stex_key_method_tl}
* 1797 }
* 1798 }
* 1790 }
* 1791 \cs_new_protected:Nn \_stex_proof_html_env:n {
* 1792 \exp_args:Nne \begin{stex_annotate_env}{
* 1793 \stml:#1={* {seq_if_empty:NF\l_stex_fors_seq {
205} {seq_use:Nn\l_stex_fors_seq,
206} }
207} } bool_if:NT\l_stex_key_hide_bool {,
208shtml:proofhide=true
210} }
211} } __stex_proof_html:
212} } ```
213}
214
215\bool_set_false:N\l_stex_proof_in_spfblock_bool
216\cs_new_protected:Nn\_stex_proof_begin_proof:nn {par
217\intarray_gzero:N\l_stex_proof_counter_intarray
218\intarray_gset:Nnn\l_stex_proof_counter_intarray 1 1
219\stex_keys.set:nn{spfsteps}{#1}
220\_stex_do_for_list:
221\stex_if_do_html:T {
222\_stex_proof_html_env:n{proof}
223} }
224\seq_map_inline:Nn\l_stex_fors_seq {
225\stex_debug:nn{definiens}{Adding-definiens-to-##1}
226\_stex_add_definiens:nn {##1}{STEXinvisible{proven}}
227} } }
```
228\stex_style_apply:
229\stex_do_id:
230\stex_reactivate_macro:N\subproof
231\stex_reactivate_macro:N\spfstep
232\stex_reactivate_macro:N\conclude
233\stex_reactivate_macro:N\assumption
234\stex_reactivate_macro:N\eqstep
235\stex_reactivate_macro:N\yield
236\stex_reactivate_macro:N\spfblock
237\stex_reactivate_macro:N\spfjust
238\stex_annotate:nn{shtml:prootiftle={}}{#2}
239\stex_if_do_html:T{
240\begin{stex_annotate_env}{shtml:proofbody={}}
241} }
242} }
243\stex_new_stylable_env:nnnnnnn{proof}{0{}m}{
244\_stex_proof_begin_proof:nn{#1}{#2}
245\bool_set_true:N\l\_stex_proof_in_spfblock_bool\_stex_proof_start_list:n{}
246\group_begin:!stexcommentfont
247}{
248\stex_style_apply:
249\stex_if_do_html:T{end{stex_annotate_env}}end{stex_annotate_env}}
250}{
251\emph{synproofautorefname :}-
252}{
253\spproofend
254}{s}
255\addToHook{env/spproof/end}{
256\bool_if:NT\l_stex_proof_in_spfblock_bool {
257\group_end:\_stex_proof_end_list:





* %symbolef{module-type}[args=i,op=\mathtt{MOD}]
* %mathopen{{comp{multtt{MOD}}}#1{mathclose{{comp()}}}}
* %symbolef{module-type-merge}[args=a,op=\opplus]
* %argsep{#1}{mathbin{comp{{oplus}}}}
* %symdef{anonymous-record}[args=a] {{nthopen{{comp[[[]}#1{mathclose{{comp[]}}}}}
* %symdef{record-field}[args=2]{#1{comp{.}#2}
* %symdecl*(record-type)
* %symdecl*(mathstruct){name=mathematical-structure,args=a] % TODO
* %notation{mathstruct}[angle,prec=nobrackets] {mathopen{{comp[angle]}#1{mathclose{{comp}rangle}}
* %notation{mathstruct}[parens,prec=nobrackets] {mathopen{{comp}#1{mathclose{{comp}}}}
* %sequences
* %symdef{ellipses}[ldots]{}}
* %symdef{sequence-expression}[comma,args=a]{#1}
* %symdef{sequence-type}[args=1]{#1^{comp{ast}}}
* %symdef{sequence-map}[args=ia]{ {comp{{m}#1{mathpunct{{comp{,}}}
* #2}mathclose{{comp}}}}
* %infalse % binder (%forall, %Pi, %lambda etc.) %symdef{pibind}[name=dependent function type,prec=nobrackets, op=(<dot);{to};{dot,args=Bi,assoc=pre}
* %argmap{#1}{mathopen{{comp()##1{mathclose{{comp()}}}}}
* %{mathbin{{comp{\{to}}}}} %mathbin{{comp{to}}#2}
* %notation{pibind}[forall]{{comp{forall#1{mathpunct{{comp.}}#2}
* %notation{pibind}[Pi]{{mathop{{comp}prod}}c_math_subscript_token{#1}#2}
* %symdef{mapbind}[name=lambda,mapsto,prec=nobrackets,op=\mapsto,args=Bi,assoc=pre] {#1{mathrel{comp}mapsto}#2}
* %notation{mapbind}[lambda,prec=nobrackets,op=\lambda] {complambda #1{mathpunct{{comp.}}#2}
* %fi %symdecl{bind}[args=Bi,assoc=pre] {notation{bind}[depfun,prec=nobrackets,op=(<dot)];{to};<dot] {mathopen{{comp}#1{mathclose{{comp}}}}}#2}
* %notation{bind}[forall]{{comp}forall#1.{};#2}
* %notation{bind}[Pi]{{mathop{{comp}prod}c_math_subscript_token{#1}#2}
* %proof{implicit-bind}[args=Bi,assoc=pre]{{mathopen{{comp}{}#1 {mathclose{{comp{{}}}}c_math
* %proof{{comp}{{name=proposition}}{{mathtt{{Prop}}}}




## Chapter 14 Additional Packages

### 14.1 Implementation: The notesslides Package

#### Class and Package Options

We define some Package Options and switches for the notesslides class and activate them by passing them on to beamer.cls and omodoc.cls and the notesslides package. We pass the nontheorem option to the statements package when we are not in notes mode, since the beamer package has its own (overlay-aware) theorem environments.

```
7650{*cls}
7660{@0=notesslides}
7661{ProvidesExplClass{notesslides}{2023/03/19}{3.3.0}{notesslides Class}
7662{RequirePackage{l3keys2e}
7663}
764{str_const:Nn\c_notesslides_class_str {article}
7666}
766{keys_define:nn{notesslides / cls}{
7667class.str_set_x:N = \c_notesslides_class_str,
7668notes.bool_set:N = \c_notesslides_notes_bool,
7669slides.code:n = {\bool_set_false:N\c_notesslides_notes_bool },
7670%docopt.str_set_x:N = \c_notesslides_docopt_str,
7671unknown.code:n = {
7672{}PassOptionsToClass{\CurrentOption}{beamer}
7673{}PassOptionsToClass{\CurrentOption}{c_notesslides_class_str}
7674{}PassOptionsToPackage{\CurrentOption}{notesslides}
7675{}PassOptionsToPackage{\CurrentOption}{stex}
7676}
7677{}
7678{}ProcessKeysOptions{ notesslides / cls }
7679
7680{RequirePackage{stex}
7681{stex_if_html_backend:T {
7682}bool_set_true:N\c_notesslides_notes_bool
7683}
7684
7685{bool_if:NTF\c_notesslides_notes_bool {
76866}PassOptionsToPackage{notes=true}{notesslides}
7687{message{notesslides.cls:-Formatting-document-in-notes-mode}


* [74] \ntesfalse
* [75] \cs_new_protected:Nn \_ntesslides_do_sectocframes: {
* [76] \cs_set_protected:Nn \_ntesslides_do_label:n {
* [77] \str_case:nnF{##1}{
* [78] {part} {
* [79] {\tl_set:Nxl_ntesslides_num{\thepart}
* [79] \tl_set:cx{@@label}{
* [80] \cs_if_exist:NTF}partitlename{exp_not:N}parttitlename}{exp_not:N}partname}{}
* [79] {charter} {
* [79] {\tl_set:Nxl_ntesslides_num{\thechapter}
* [80] \tl_set:cx{@@@label}{
* [81] \cs_if_exist:NTF}chaptertitlename{exp_not:N}chaptertitlename}{exp_not:N}chapter
* [82] \
* [83] \
* [84] \cs_if_exist:NTF}chaptertitlename{exp_not:N}chaptertitlename}{exp_not:N}chaptertitlename}{
* [85] \
* [86] \
* [87] \tls_set:Nxl_ntesslides_num{\cs_if_exist:NT}thechapter{\thechapter.}\tlssection}
* [88] \tl_set:cx{@@@label}{\l_ntesslides_numQuad}
* [89] \
* [80] \tls_set:Nxl_ntesslides_num{\cs_if_exist:NT}thechapter{\thechapter.}\tlssection.
* [80] \tls_set:cx{@@@label}{\l_ntesslides_numQuad}
* [81] \tls_set:Nxl_ntesslides_num{\cs_if_exist:NT}thechapter{\thechapter.}\tlssection.
* [82] \tls_set:Nxl_ntesslides_num{\cs_if_exist:NT}thechapter{\thechapter.}\tlssection.
* [83] \tls_set:Nxl_ntesslides_num{\cs_if_exist:NT}thechapter{\thechapter.}\tlssection.
* [84] \tls_set:Nxl_ntesslides_num{\cs_if_exist:NT}thechapter{\thechapter.}\tlssection.
* [85] \tls_set:Nxl_ntesslides_num{\cs_if_exist:NT}thechapter{\thechapter.}\tlssection.\tls_set:cx{@@label}{\l_ntesslides_num}quad}
* }
* [86] \cs_set_protected:Nn \_sfragment_do_level:nn {
* [87] \tl_if_exist:CT{c@#1}{stepcounter{##1}}
* \addcontentsline{toc}{##1}{protect}numberline{\use:c{the##1}}##2}
* \_notesslides_do_label:n{##1}
* [88] \pdfbookmark[\int_use:N \l_stex_docheader_sect]{\l_ntesslides_num}##2}{##1.\l_note

[MISSING_PAGE_POST]


#### Notes and Slides

For the notes case, we also provide the \usetheme macro that would otherwise come from the the beamer class.

```
7851\bool_if:NT\c_notesslides_notes_bool{
7854\renewcommand\usetheme[2][\{\usepackage[#1]{beamertheme#2}}
7855\
7856\NewDocumentCommand\libusetheme{0{}m}{
7857\libusepackage[#1]{beamertheme#2}
7858}
```

We define the sizes of slides in the notes. Somehow, we cannot get by with the same here.

```
7851\enlength{slidewidth}{slidewidth}{13.5cm}
7856\enlength{slideheight}{slideheight}{9cm}
```

We first set up the slide boxes in notes mode. We set up sizes and provide a box register for the frames and a counter for the slides.

```
7851\infnotes
7852\enlength{slideframework}
7854\setlength{slideframework}{1.5pt}
```

frame(_env._) We first define the keys.

```
7856\cs_new_protected:Nm\_notesslides_do_yes_param:Nn{
7856\exp_args:Nx\str_if_eq:nmTF{ustr_uppercase:n{#2}}{yes}{
7857\bool_set_true:N#1
7858\f{
7859\bool_set_false:N#1
7860\
7871\
7872
7873\stex_keys_define:nnnnn{notesslides/frame}{
7874\str_clear:N\l_notesslides_frame_label_str
7875\bool_set_true:N\l_notesslides_frame_allowframeshreshold
7876\bool_set_true:N\l_notesslides_frame_flagile_bool
7878\bool_set_true:N\l_notesslides_frame_shrink_bool
7879\bool_set_true:N\l_notesslides_frame_squeeze_bool
7880\bool_set_true:N\l_notesslides_frame_t_bool
7881\f{
7882label\.str_set_x:N=\l_notesslides_frame_label_str,
7883allowframebreaks.code:n={


7934 \medskippar\noindent\tiny\notesslidesfooter
7935 \end{stex_annotate_env}\egroup
7936 \}
7937 \cs_new_protected:Nn\_notesslides_frame_box_begin:{
7939 \begin{mdframed}[
7940 \linewidth=\slideframewidth,
7941 \skipabove=1ex,
7942 \skipbelow=1ex,
7943 \userdefinedwidth=\slidewidth,
7944 \align=center
7945 \notesslidesfoot \
7946 \}
7947 \cs_new_protected:Nn\_notesslides_frame_box_end:{
7948 \medskippar\noindent\tiny\notesslidesfooter%~^\notesslides%slidelabel
7940 \end{mdframed}
7950 \}
7951 \

We define the environment, read them, and construct the slide number and label.

7952 \renewenvironment{frame}[1][ \{
7953 \stex_keys_set:nn[notesslides/frame}{#1}
7954 \stepcounter{framenumber}
7955 \renewcommand\newpage{addtocounter{framenumber}{1}}
7956 \def\@currentlabel{theframenumber}
7957 \str_if_empty:NF\1_notesslides_frame_label_str{
7958 \label{l}_notesslides_frame_label_str}
7959 \notesslides_setup_itemize:
7951 \notesslides_frame_box_begin:
7952 \notesslides_frame_box_end:
7954 }

Now, we need to redefine the frametitle (we are still in course notes mode).

\framettitle
7965 \renewcommand{frametitle}[1]{
7966 \stexdoctitle{#1}
7967 \notesslidestitleemph{#1}\medskip
7968 \notesslidestitleemph{#1}\medskip
7966 \} (End definition for \framettitle. This function is documented on page??.)

\pause
7969 \newcommand\pause{} (End definition for \pause. This function is documented on page??.)

We redefine the columns and column environments:

\frametenvironment{columns}[1][ \{
7971 \par\noindent\framed}
7972 \begin{minipage}
7973 \slidewidth\centering\leavevmode
7974 \% \stex_if_html_backend:T{

#### 14.1.3 Environment and Macro Patches

The note environment is used to leave out text in the slides mode. It does not have a counterpart in OMDoc. So for course notes, we define the note environment to be a no-operation otherwise we declare the note environment to produce no output.

```
8014\bool_if:NTF\c_notesslides_notes_bool{
8015\renevenvironment{note}{ignorespaces}{}
8016}{\renevenvironment{note}{setbox\l_tmpa_box\vbox\bgroup}{\egroup}
8018}
```

For other environments we introduce variants prefixed with n, which are excluded in slides mode.





```
1002test.default:n={true},
1003test.bool_set:N=\c__problems_test_bool,
1004unknown.code:n={
1026\PassOptionsToPackage{CurrentOption}{stext}
1026}
1027}
1028Unewif{ifsolutions
1030
1040
10510ProcessKeysOptions{problem/pkg}
1061\bool_if:NTF\c__problems_solutions_bool{
1071\solutionstrue
1072}{
1073\solutionsfalse
10745}
1075
1086\RequirePackage{stext}
```

```
\problem@kw@*Formultilinguality, we define internal macros for keywords that can be specialized in *.1df files.
1021\AddToHook{begindocument}{
10218\ExplSyntaxOn\makeatletter
10219\input{problem-english.ldf}
10220\ltx@ifpackageloaded{babel}{
10221\clist_set:Nx\l_tmpa_clist{\bbl@loaded}
10222\exp_args:NNx\clist_if_in:NnT\l_tmpa_clist{\detokenize{ngerman}}{
1023\input{problem-ngerman.ldf}
1024\exp_args:NNx\clist_if_in:NnT\l_tmpa_clist{\detokenize{finnish}}{
1025\input{problem-finnish.ldf}
1026\exp_args:NNx\clist_if_in:NnT\l_tmpa_clist{\detokenize{french}}{
1027\input{problem-french.ldf}
1028\exp_args:NNx\clist_if_in:NnT\l_tmpa_clist{\detokenize{russian}}{
1029\input{problem-russian.ldf}
1030\}
10312\makeatother\ExplSyntaxOff
10323}
```

(_End definition for\problem@kw@*. This function is documented on page??.)

#### Problems and Solutions

We now prepare the KeyVal support for problems. The key macros just set appropriate internal macros.

``` \t_set:Nn\l_stext_key_pts_tl0
1023\tl_set:Nn\l_stext_key_min_tl0
1034\str_clear:N\l_stext_key_name_str
1041\str_clear:N\l_stext_key_mhrepos_str
1042}{
1053pts.tl_set:N=\l_stext_key_pts_tl,
1054min.tl_set:N=\l_stext_key_min_tl,name.str_set:N = \l_stex_key_name_str,
824 archive.str_set:N = \l_stex_key_mhrepos_str,
825 creators.code:n = {}
826%imports.tl_set:N = \l_problems_prob_imports_tl,
827%refnum.int_set:N = \l_problems_prob_refnum_int,
8280 }{id,title,style,uses} Then we set up a counter for problems.

```
1numberproblemsin
1
111 \newcounter{problem}[section]
112 \newcommandnumberproblemsin[1]{
113 \addtoreset{problem}{#1}
114 \def\theproblem{\arabic{#1}.\arabic{problem}}
115 \numberproblemsin{section}
116 %def\theplainsproblem{\arabic{problem}}
117 %def\theproblem{\thesection.\theplainsproblem}
```

(_End definition for_\numberproblemsin. This function is documented on page??.)

```
1sproblem (env.)
118 \newcounter{pts}
119 \newcounter{min}
120 \stex_new_stylable_env:nnnnnnn {problem}{0}}
121 \cs_if_exist:NTF \l_problem_inputproblem_keys_tl {
122 \tl_put_left:Nn \l_problem_inputproblem_keys_tl {#1,}
123 \exp_args:Nno \stex_keys_set:nn{problem}{
124 \l_problem_inputproblem_keys_tl }
125 \t
126 \stex_keys_set:nn{problem}{#1}
127 \refstepcounter{problem}
128 \stex_if_empty:NT \l_stex_key_name_str {
129 \stex_file_split_off_lang:NN \l_problems_path_seq \g_stex_current_file
130 \seq_get_right:NN \l_problems_path_seq \l_stex_key_name_str }
131 \exp_args:No \stex_module_setup:n \l_stex_key_name_str
132 \stex_if_do_html:T {
133 \exp_args:Nne \begin{stex_annotate_env} {
134 \shtml:problem={\l_stex_current_module_str},
135 \shtml:language={\l_stex_current_language_str},
136 \stml:signature={\l_stex_key_sig_str}
137 \tl_if_empty:NF \l_stex_metatheory_uri {,
138 \shtml:metatheory={stex_uri_use:N \l_stex_metatheory_uri}
139 }
130 \stex_annotate_invisible:n{}
131 \tl_if_empty:NF \l_stex_key_title_tl {
132 \exp_args:No \stexdoctitle \l_stex_key_title_tl }
133 }









#### 14.3.2 Assignments

Then we set up a counter for problems and make the problem counter inherited from problem.sty depend on it. Furthermore, we specialize the \prob@label macro to take the assignment counter into account.

assignment (_env._)

```
866%stexkeys_define:nnnnn{assignment}{
867%tl_clear:N\l_stexkey_number_tl
868%tl_clear:N\l_stexkey_given_tl
869%tl_clear:N\l_stexkey_due_tl
870%
871number.tl_set:N=\l_stexkey_number_tl,
872%given.tl_set:N=\l_stexkey_given_tl,
873%due.tl_set:N=\l_stexkey_due_tl,
874%unknown.code:n={}
875%id,title,style}
876%newcounter{assignment}
877%stex_new_stylable_env:nnnnnnn{assignment}{
878%cs_if_exist:NTF\l_hvexam_includeassignment_keys_tl{
879%tl_put_left:Nn\l_hvexam_includeassignment_keys_tl{#1,}
89%exp_args:Nno\stexkeys_set:nn[assignment]{
990%l_hvexam_includeassignment_keys_tl }
910%stexkeys_set:nn[assignment]{#1}
921%tl_if_empty:NF\l_stexkey_number_tl{
930%global\setcounter{assignment}{\int_eval:n{\l_stex_key_number_tl-1}}
931%global\refstepcounter{assignment}
932%setcounter{problem}{0}
933%def\theproblem{\theassignment.\arabic{problem}}
934%stex_style_apply:




















964, 965, 2338, 2481, 3122, 3127, 3128, 3141, 3146, 3147, 7453, 7534 \l_stex_current_redo_tl.................. 5163, 5176, 5187, 5190, 5197, 5327, 6323, 6361, 6396, 6546 \l_stex_current_return_tl.......... _120_, 3955, 5183, 5249, 5261, 5282, 5332 \stex_current_section_level.............. 1272, 1278, 1287, 1313, 7789 \l_stex_current_symbol_str.............. 120, 4147, 4177, 4296, 4336, 4347, 4445, 4464, 4527, 4753, 4905, 4907, 4913, 4948, 5038, 5041, 5056, 5084, 5085, 5168, 5180, 5202, 5218, 5247, 5248, 5251, 5257, 5273, 5274, 5277, 5366, 5448, 5475, 5492, 5594, 5595, 5638, 5679, 5680, 5712, 5725, 5742, 5767, 5775, 5796, 5804, 5857, 5862, 5935, 5948, 5961, 5971, 5


4865, 5213, 6139, 6147, 6197, 6736 \stex_get_var:n _114_, 4432, 4857, 4886, 5933, 5944, 5957, 7023 \c_stex_home_file _127_, 1035 \stex_if_check_terms: _113_, 3628, 3639, 3643 \stex_if_check_terms:TF _113_, 3627, 3648, 4121, 4435, 4742, 4938, 4941 \stex_if_check_terms_p: _113_, 3627 \stex_if_do_html: _275 \stex_if_do_html:TF _129_, 272, 284, 1248, 1275, 1284, 1528, 2499, 2519, 2757, 2773, 2803, 2851, 3036, 3260, 3301, 3337, 3371, 3725, 3909, 3921, 4123, 4482, 4736, 4744, 4790, 4937, 6158, 6214, 6742, 6800, 7024, 7221, 7239, 7249, 7266, 7276, 7310, 7317, 7319, 7357, 7578, 7603, 7635, 8278, 8309, 8367, 8376, 8386, 8392, 8424, 8433, 8443, 8449, 8473, 8482, 8492, 8498, 8522, 8531, 8541, 8547, 8573, 8582, 8628, 8635, 8644 \stex_if_do_html_p: _129_ \stex_if_file_absolute:N _126_, 741, 751 \stex_if_file_absolute:NTF _126_, 739, 985, 1070 \stex_if_file_absolute_p:N _126_, 739 \stex_if_file_starts_with:NNF _126_, 761 \stex_if_file_starts_with:NNTF _126_, 761, 1193 \stex_if_html_backend:TF _129_, 289, 314, 321, 330, 613, 1248, 1292, 1354, 1373, 1420, 1927, 1954, 3627, 5160, 5194, 5706, 5762, 5791, 5969, 5995, 6843, 6853, 6929, 7681, 7721, 7846, 7926, 7974, 7982, 7994, 8004, 8114 \stex_if_html_backend_p: _129_, 289 \stex_if_in_module: _129_, 289 \stex_if_in_module: _12523_ \stex_if_in_module:TF _111_, 2275, 2523, 2539 \stex_if_in_module_p: _111_, 2523 \stex_if_in_module_exists:n _1252_ \stex_if_module_exists:nTF _111_, 2292, 2305, 2527, 3124, 3127, 3143, 3146, 3231, 6148, 6198, 6737 \stex_if_module_exists_p:n _111_, 2527 \stex_if_smsmode: _2113_ \stex_if_smsmode:TF _124_, 431, 1240, 1514, 2111, 2178, 2311, 2510, 2518, 3040, 3183, 3209, 3264, 3305, 3457, 3464, 3477, 3485, 3501, 3509, 3571, 3591, 3612, 3702, 3930, 4132, 4485, 6836, 6852, 6878, 6905, 7008, 8292, 8308 \stex_if_smsmode_p: _124_, 2111 \stex_ignore_spaces_and_pars: _131_, 351, 351, 354, 2549, 2550, 8319 \l_stex_import_archive_str _119_, 2451, 2456, 2788, 3033, 3058, 3062, 3083, 3084, 3252, 3279, 3295 \stex_import_module_uri:nn _119_, 2449, 2785, 3031, 3049, 3049, 3250, 3276, 3293 \l_stex_import_name_str _119_, 2453, 2458, 2790, 3035, 3043, 3052, 3254, 3268, 3281, 3297, 3309 \l_stex_import_ns_str _2459_, 2462, 2792, 3038, 3042, 3125, 3128, 3131, 3144, 3147, 3150, 3158, 3256, 3259, 3262, 3267, 3299, 3303, 3308, 3259, 3207, 3299, 3303, 3308, 3308, 3309, 3304, 3053, 3064, 3068, 3072, 3073, 3074, 3077, 3253, 3280, 3296 \stex_import_require_module:nnn _119_, 2455, 2787, 3032, 3087, 3087, 3100, 3251, 3294 \stex_import_require_module_-safe:nnn _123_, 3278 \l_stex_import_uri_str _119_, 3063, 3084, 3090, 3095, 3105, 3110, 3118, 3120, 3124, 3125, 3131, 3137, 3139, 3143, 3144, 3150, 3169, 3176, 3196, 3231, 3232 \stex_in_archive:nn _123_, 1086, 1086, 1875, 1926, 1951, 2005, 2058 \stex_in_invisible_html_bool _... _3766_, 4811, 5704, 5705, 5735 \l_stex_in_meta_bool _2354_, 2355, 2360 \l_stex_inparray_bool _... _5835_\stex_input_with_hooks:n _... _1014_, 1877, 1880, 1901, 1918, 1920 \stex_invoke_notation:w _... _5123_, 5240, 5241, 5246, 5283 \stex_invoke_outer_field: _... _6122_\stex_invoke_sequence: _... _4967_, 4980, 5031, 5031, 5572 \stex_invoke_sequence_in: _121_\stex_invoke_structure: _... _6090_, 6138, 6258 \stex_invoke_symbol: _... _... _114_, 120_, 3739, 4772, 4785, 5217, 5217, 6798, 7625 \stex_invoke_order_120_12_13, 1200, 1211, 1211, 1211, 1211, 1211, 1211, 1211, 1211, 1211, 1211, 1211, 1211, 1211, 1211, 1211, 12111, 1211, 12111, 12111, 1211, 1211, 1211, 12111, 1211, 12111, 1211, 12111, 1211, 12111, 12111, 12111, 12111, 12111, 12111, 12111, 12111, 1211


\l_stex_key_proof_tl 5882 \l_stex_key_pts_tl........ 8238, 8243, 8297, 8313, 8336 \l_stex_key_reorder_str 3662, 3666, 3759, 3760, 4803, 4804, 5000, 5001 \l_stex_key_return_tl........ 3677, 3682, 3738, 3773, 3776, 3869, 4740, 4771, 4784, 4818, 4821, 4929, 4966, 4979, 5011, 5014, 6758 \l_stex_key_role_str........ 3661, 3669, 3762, 3763, 3894, 4800, 4801, 4997, 4998, 6792 \l_stex_key_root_tl 5886 \l_stex_key_short_tl........ 1307, 1310, 1337, 1339 \l_stex_key_sig_str........ 111, 2281, 2323, 2471, 2486, 2503, 8282 \l_stex_key_style_clist........ 122, 399, 401, 451, 455, 502, 506, 6826, 6827, 6920 \l_stex_key_T_bool........ 8596, 8602, 8604, 8617, 8637 \l_stex_key_term_tl........ 7063, 7073, 7192, 7193, 7343, 7347 \l_stex_key_title_str........ 6764 \l_stex_key_title_tl........ 393, 395, 1563, 1741, 1742, 2493, 6840, 6845, 8288, 8289, 8295, 8359, 8401, 8402, 8416, 8458, 8459, 8465, 8507, 8508, 8514, 8556, 8557, 8730, 8731 \l_stex_key_Ttext_tl 8597, 8605, 8618 \l_stex_key_type_tl....... 114, 3675, 3685, 3706, 3737, 3767, 3768, 3865, 3877, 3881, 4458, 4770, 4783, 4812, 4813, 5005, 5006, 6756, 6765 \l_stex_key_variant_str........ 115, 4102, 4108, 4114, 4142, 4195, 4308, 4317, 4349, 4443, 4462, 4751, 4842, 4850, 4946 \stex_keys_define:nnnn....... 121, 359, 359, 378, 386, 392, 398, 404, 410, 1336, 1547, 1553, 2470, 3659, 3672, 3875, 4101, 4453, 4719, 5879, 6069, 6751, 7058, 7339, 7873, 8237, 8341, 8594, 8696, 8795 \stex_keys_set:nn.... 121, 122, 374, 374, 1343, 1565, 1766, 1771, 2492, 3694, 3886, 3887, 4118, 4431, 4472, 4726, 4919, 5891, 5899, 5910, 5932, 5943, 5956, 6080, 6833, 6862, 6956, 6962, 6970, 7148, 7219, 7274, 7377, 7573, 7607, 7953, 8264, 8268, 8351, 8615, 8711, 8715, 8750, 8808 \stex_kpsewhich:Nn 131, 36, 36, 47, 54 \c_stex_language_abbrevs_prop.......... 128, 103 \stex_language_from_file:........ 129, 151, 151, 997 \c_stex_languages_clist 23, 174, 177 \c_stex_languages_prop....... 128, 103, 131, 132, 166, 182, 798 \g_stex_last_feature_str........ 117, 2771, 6106 \stex_macro_body:N 130, 537, 539, 557 \stex_macro_definition:N 130, 552, 552 \l_stex_macroname_str....... 114, 215, 2761, 2762, 3692, 3696, 3698, 3732, 3753, 3754, 3888, 3899, 4473, 4727, 4765, 4777, 4794, 4795, 4920, 4960, 4972, 4991, 4992, 6091, 6791, 7608, 7618 \_stex_main_archive:.... 1192, 1231 \c_stex_main_archive_prop.123, 1192 \c_stex_main_file............... 126, 127, 967, 1006, 1072, 7643 \_stex_map_args:N....... 3777, 4076, 4076, 4174, 4270, 4341, 4505, 4822, 5015, 5378, 6120 \_stex_map_notation_args:N....... 4076, 4089, 4374 \stex_map_uri:Nnnnnn 127, 804, 811, 2338 \c_stex_mathhub_file 127, 911, 1035, 1111, 1121, 1134, 1193, 1611, 1690, 1701, 1853, 1865, 1877, 1880, 1904, 1909, 1920, 1972, 2022, 2026, 2036, 2040, 2050, 2055, 3096, 3111 \c_stex_mathhub_main_manifest_prop....... 1199, 1200 \stex_mathml_arg:nn.130 \stex_mathml_intent:nn.130 \_stex_maybe_brackets:nn.4558, 4575, 5039, 5275, 5286, 5828 \stex_metagroup_do_in:nn.112, 132, 225, 230, 237, 2532, 3344, 3378, 7615, 7616, 7627 \stex_metagroup_new:n.132, 219, 220, 224, 2283, 2332, 2816 \l_stex_metatheory_uri....... 2152, 2358, 2361, 2445, 2461, 2475, 2477, 2504, 2505, 7534, 7535, 7536, 7583, 7584, 8283, 8284 \c_stex_module_.112, 114 \stex_module_add_code:n.112, 2535, 2535, 2538, 2540, 2550, 7591 \stex_module_add_morphism:nnn.11 \stex_module_add_morphism:nnnnn.119, 2556, 2556, 2556, 25612, 920, 3258, 6162, 6218, 7594 \stex_data_




_stex_expr_do_ref:nNm... 5893, 5901, 5912, 5934, 5945, 5958, 5968 _stex_expr_do_seqmap:nnnnnn...... 5542, 5649 _stex_expr_end:... 5539, 5549 _stex_expr_gobble:nnnnnnnn...... 5539, 5549 _stex_expr_iarg_t1 5629, 5631, 5642 _stex_expr_invoke_custom:n...... 5224, 5238, 5365 _stex_expr_invoke_math: 5219, 5227 _stex_expr_invoke_op_custom:n... 5224, 5231, 5357 _stex_expr_invoke_op_notation:w... 5233, 5234, 5272 _stex_expr_invoke_return:...... 5313, 5316 _stex_expr_invoke_return_- maybe:n... 5255, 5265, 5294 _stex_expr_invoke_return_next:... 5301, 5310 _stex_expr_invoke_text: 5219, 5222 _stex_expr_is_seqmap:n... 5578 _stex_expr_is_seqmap:nTF... 5541 _stex_expr_is_varseq:n... 5567 _stex_expr_is_varseq:nTF 5535, 5654 _stex_expr_left_bracket_str... 5824, 5850, 5858, 5868, 5869 _stex_expr_old_seq...... 5661, 5664, 5668, 5673 _stex_expr_reset_tl...... 5135, 5138, 5142, 5143, 5149 _stex_expr_ret_cs...... 5298, 5303, 5330, 5335, 5340 _stex_expr_return_arg:n 5300, 5306 _stex_expr_return_args_tl... 5295, 5307, 5312, 5321, 5337, 5342 _stex_expr_return_notation:n...... 5318, 5351 _stex_expr_return_this_tl...... 5296, 5312, 5317, 5321, 5325, 5326, 5336, 5344 _stex_expr_right_bracket_str... 5825, 5851, 5863, 5868, 5870 _stex_expr_setup:nnnnnn...... 5161, 5173, 5195 _stex_expr_varseq_in_map:nnnnnnnn... 5656, 5695 _stex_features_add_definiens:nn...... 2828, 2971 _stex_features_break:... 2829, 2833 _stex_features_check_break:nnnnnnnnnn... 2992, 2997, 3006, 3009, 3016 _stex_features_clean:nnnw 2868, 2876 _stex_features_do_decls: 2860, 2872 _stex_features_do_elaboration:...... 2850, 2900 _stex_features_do_for_list:...... 2819, 2970 _stex_features_do_morph:nnnn...... 2948, 2952 _stex_features_do_morphisms:n... 2861, 2946, 2956 _stex_features_elab_check:...... 2908, 2931 _stex_features_feature_str...... 2811, 2923 _stex_features_get_check:nnnn... 2976, 3004 _stex_features_implicit_bool.... 2777, 2796, 2799, 2936 _stex_features_reactivate:...... 2814, 2959 _stex_features_rename:nn 2924, 2927 _stex_features_rename_all:. 2864 _stex_features_renamed_- check:nnnnnn... 2980, 2990 _stex_features_set_definiens_- macros:... 2829, 2833 _stex_features_set_definiens_- macros:innnnnnnn... 2836, 2840 _stex_features_setup:... 2813, 2856 _stex_features_split_qm:w...... 2899, 2917 _stex_features_tmp...... 2911, 2913, 2932, 2933, 2934 _stex_features_total_check:...... 2889, 2893 _stex_groups_do:... 250, 257, 266 _stex_groups_do_in:nn 232, 239, 260 _stex_groups_exists:n... 225 _stex_groups_exists:nTF... 231 _stex_groups_ids_seq 219, 222, 258 _stex_groups_tmp... 241, 248, 254 _stex_importodule_archive_- str 3089, 3094, 3104, 3109, 3226, 3227 _stex_importodule_check_- file:nn... 3170, 3171, 3172, 3173, 3174, 3175, 3197, 3198, 3199, 3200, 3201, 3202, 3236 _stex_importodule_get_from_- file:nnnn... 3130, 3166 _stex_importodule_get_from_- file_safe:nnn... 3149, 3193 _stex_importodule_get_- module:nnn... 3091, 3097, 3155 _stex_importodule_get_module_- safe:nnn... 3106, 3112, 3161





_stex_seqs_loop_range:w 5046, 5050 \l_stex_seqs_first_args_tl............ 5099, 5117, 5118, 5122, 5123 \_stex_seqs_get_index_notation:n...... 5045, 5083, 5116 \_stex_seqs_html:...... 4937, 4987 \_stex_seqs_macro:...... 4940, 4971 \_stex_seqs_make_args:.. 4950, 4984 \l_stex_seqs_range_clist...... 4930, 4965, 4978 \g_stex_smsmode_allowed_escape_- tl...... 2093, 2100, 2229 \g_stex_smsmode_allowed_import_- env_seq 2117, 2123, 2163, 2212, 2215 \g_stex_smsmode_allowed_import_- tl...... 2116, 2119, 2160, 2207 \g_stex_smsmode_allowed_tl...... 2092, 2096, 2225 \g_stex_smsmode_allowedenv_seq...... 2094, 2104, 2234, 2237 \g_stex_smsmode_bool...... 2111, 2112, 2114, 2130 \_stex_smsmode_check_begin:Nn...... 2212, 2234, 2246 \_stex_smsmode_check_cs:NNn...... 2185, 2193 \_stex_smsmode_check_end:Nn...... 2215, 2237, 2255 \_stex_smsmode_do:w...... 2179, 2191, 2193, 2195, 2217, 2227, 2239, 2252, 2259, 2262 \_stex_smsmode_do_aux:N. 2193, 2199 \_stex_smsmode_do_aux_curr:N...... 2159, 2170, 2201 \_stex_smsmode_do_aux_imports:N...... 2159, 2205 \_stex_smsmode_do_aux_normal:N...... 2170, 2223 \l_stex_smsmode_importmodules_- seq...... 2148 \_stex_smsmode_in_smsmode:n...... 2128, 2158, 2168, 2169 \l_stex_smsmode_sigmodules_seq 2149 \_stex_smsmode_smsmode_do:...... 2141, 2177 \l_stex_smsmode_start_smsmode:n...... 2139, 2166, 2171 \_stex_statements_do_defref:nn...... 6928, 6957, 6963, 6971 \_stex_statements_force_id:...... 6787, 6890, 6898, 6921 \_stex_statements_html_keyvals:nn...... 6817, 6838, 6866 \_stex_statements_setup:nn...... 6779, 6899, 6904, 6918, 6922, 6925 \_stex_statements_setup_def:...... 6877, 6900, 6923 \l_stex_statements_trial_str...... 6802, 6806, 6807, 6812, 6813, 6983, 6989, 6991, 7036, 7039, 7042 \l_stex_structures_assigned_seq................6465, 6576, 6615, 6631 \_stex_structures_begin:nn...... 6062, 6079, 6156, 6211 \_stex_structures_check_- def:nnnnnnnnnn...... 6230, 6243 \l_stex_structures_clist...... 6439, 6460, 6466, 6468 \l_stex_structures_comp_cs...... 6508, 6513 \l_stex_structures_cs...... 6441, 6447, 6454 \l_stex_structures_current_type:................6395, 6526, 6597 \l_stex_structures_current_- type_tl.... 6322, 6358, 6398, 6403 \_stex_structures_do_assign:nn...... 6342, 6346 \_stex_structures_do_assign_- list:n................6318, 6339 \_stex_structures_do_decl:nnnnnnnnnnnn...... 6653, 6673 \_stex_structures_do_decl_- nomacro:nnnnnnnnn...... 6651, 6659 \_stex_structures_do_externals:................6066, 6104, 6171, 6233 \_stex_structures_end:................6286, 6290, 6306, 6311 \l_stex_structures_exstruct_- name_str...... 6206, 6211, 6255 \_stex_structures_extend_- structure:nn...... 6183, 6206 \_stex_structures_extend_- structure_i:NnnnnnnnnN...... 6180, 6188 \_stex_structures_external_- decl:nnnnn...... 6107, 6111 \l_stex_structures_extmod_str...... 6181, 6185 \l_stex_structures_extname_- count...... 6249, 6253, 6255 \l_stex_structures_field_name_- str...... 6563, 6567, 6568, 6599 \l_stex_structures_fields_clist...... 6319, 6340, 6347, 6365, 6368, 6622, 6623 \_stex_structures_get_field_- name:n................6562, 6574 \_stex_structures_get_field_-\1_stex_structures_imports_seq......... 6144, 6149, 6157, 6194, 6199, 6213, 6735, 6738, 6741 \_stex_structures_invokation_  type:n................ 6270, 6317 \_stex_structures_invoke_  field:n................ 6540, 6572 \_stex_structures_invoke_  field:nn................ 6529, 6533 \_stex_structures_invoke_this:n................ 6279, 6521 \_stex_structures_invoke_top:n................ 6260, 6263, 6287, 6291, 6294, 6297, 6299 \_stex_structures_make_mod:n................................ 6364, 6376 \_stex_structures_make_oml:n................................ 6368, 6382 \_stex_structures_make_oml:nn................................ 6383, 6385 \_stex_structures_make_prop:................... 6407, 6534, 6612 \_stex_structures_make_prop_................ 6327, 6334, 6350 \_stex_structures_make_type:n................ 6327, 6332, 6334, 6350 \_stex_structures_maybe_  notation:w................ 6274, 6276, 6402 \_stex_structures_merge:nw................................ 6268, 6284 \l_stex_structures_more_  nextsymbol_tl................ 6575, 6577, 6602 \l_stex_structures_name_str................ 6054, 6071, 6075, 6081, 6082, 6087, 6088, 6093, 6094, 6097, 6113, 6119 \_stex_structures_new_extstruct_  name:................ 6193, 6251 \_stex_structures_present:................................ 6413, 6538 \_stex_structures_present:nn................................ 6417, 6423, 6428, 6435, 6438 \_stex_structures_present_  entry:nn................ 6443, 6449, 6464 \_stex_structures_present_i:w................................ 6409, 6415, 6421 \_stex_structures_present_ii:nw................................ 6426, 6434 \l_stex_structures_prop................................ 6453, 6565, 6573, 6605, 6613, 6630, 6633, 6639, 6660, 6662, 6674, 6676 \_stex_structures_prop_do_  decls:................ 6617, 6648 \_stex_structures_prop_do_  notations:................ 6618, 6697 \l_stex_structures_prop_do_ \l_stex_structures_prop_do_  actions:................ 6618, 6697 \l_stex_structures_prop_do_ \l_stex_structures_prop_do_ \l_stex_structures_prop_do_ \l_stex_structures_prop_do_ \l_stex_structures_prop_do_ \l_stex_structures_prop_do_ \l_stex_structures_introduces:................ 6614, 6661, 6642, 6689, 6700, 6715 \l_stex_structures_replace_  this_tl................ 6105 \l_stex_structures_seq................................ 6614, 6661, 6675, 6699 \l_stex_structures_set_comp_tl................................ 6259, 6308, 6312, 6470, 6587 \_stex_structures_set_custom_  comp:n................ 6313, 6502 \_stex_structures_set_customcomp:n................ 6312, 6502 \_stex_structures_set_customcomp:................ 6286, 6311 \_stex_structures_set_customcomp:................ 6286, 6311 \_stex_structures_set_this:n................................ 6535, 6544 \_stex_structures_set_thiscomp:................ 6259, 6496 \_stex_structures_set_thisnotation:................ 6290, 6306 \_stex_structures_shift_ \l_stex_structures_shift_ \l_stex_symbol_tl................................ 6120, 6125 \l_stex_structures_this_tl................................ 6271, 6471, 6472, 6475, 6490, 6547, 6550, 6557, 6578, 6579, 6582, 6596 \_stex_symbol_add_decl: 3724, 3730 \_stex_symbol_crgs_tl 3777, 3779 \l_stex_symbol_crgs_tl................ 3775, 3779, 3969, 3971, 3973, 3999 \_stex_symbol_cl_do_args: 3794, 3853 \_stex_symbol_env_str................ 3632, 3633, 3634 \_stex_symbol_get_from_one_  string:n................ 4008, 4053 \_stex_symbol_get_symbol_from_ - cs:................ 3975, 3986 \_stex_symbol_get_symbol_from_ - modules:nn................ 4010, 4042 \_stex_symbol_get_symbol_from_ - string:n................ 3976, 3978, 3981, 4003 \l_stex_symbol_seq_symbol_from_ - string:n................ 3979, 3978, 3981, 4003 \l_stex_symbol_seq_symbol_from_ -................ 4005, 4006, 4007, 4011 \_stex_symbol_set_textsymdecl_ - macro:nn................ 3926, 3944 \_stex_symbol_sym_from_str_ - i:nnnn................ 4016, 4047 \_stex_symbol_syn_i_finish:nnnnnnnnnN................ 4022, 4029


6786, 6803, 6823, 6891, 6986, 7039, 7286, 7295, 7364, 7378, 7384, 7609, 7735, 7794, 7957, 8271, 8361, 8401, 8418, 8418, 8458, 8467, 8507, 8516, 8556 %str_if_empty:nTF...... 465, 492, 676, 727, 822, 1500, 1851, 2474, 3375 %str_if_eq:NNTF...... 165, 776 %str_if_eq:nnTF...... 139, 155, 156, 157, 179, 295, 528, 533, 563, 579, 588, 600, 606, 690, 728, 729, 745, 1624, 1708, 1750, 1755, 1757, 1808, 2261, 2343, 2582, 2615, 2720, 2991, 2996, 3005, 3008, 3184, 3210, 3394, 3410, 3634, 4212, 4224, 4236, 4877, 4880, 5071, 7003, 7798, 7801, 7866, 8025, 8588 %str_if_eq_p:nn 4018, 4019, 4058, 4059 %str_if_exist:NTF...... 226, 1834 %str_if_in:NnTF...... 4290, 5973, 6935 %str_item:Nn...... 690, 745, 3858 %str_lowercase:n...... 8588 %str_map_break:...... 3804 %str_map_break:...... 3805, 3809, 3813, 3817, 3821, 3825, 3829, 3833, 3837 %str_map_inline:Nn...... 3802 %str_new:N......... 128, 1555, 1556, 2019, 2266, 3692 %str_put_right:Nn...... 7099 %str_range:Nnn...... 2013 %str_range:nnn...... 529, 534, 568 %str_replace_all:Nnn...... 689 %str_set:Nn...... 41, 49, 130, 178, 221, 683, 684, 687, 703, 820, 1077, 1160, 1172, 1173, 1502, 1504, 1506, 1570, 1571, 1599, 1610, 1618, 1625, 1689, 1695, 1700, 1706, 1715, 1853, 1860, 1865, 1976, 1984, 2011, 2049, 2300, 2316, 2339, 2409, 2638, 2792, 2797, 2800, 2811, 2834, 2835, 3018, 3019, 3020, 3053, 3058, 3063, 3063, 3068, 3074, 3082, 3084, 3090, 3094, 3095, 3096, 3105, 3109, 3110, 3111, 3118, 3125, 3128, 3131, 3137, 3144, 3147, 3150, 3168, 3195, 3240, 3438, 3528, 3534, 3538, 3668, 3698, 3720, 3807, 3811, 3815, 3819, 3823, 3827, 3831, 3835, 3839, 3888, 3890, 3892, 3894, 3990, 3991, 4031, 4032, 4063, 4064, 4143, 4172, 4177, 4296, 4336, 4347, 4473, 4727, 4729, 4861, 4905, 4907, 4920, 4922, 4925, 5180, 5181, 5594, 5638, 5679, 5971, 5974, 6053, 6082, 6091, 6185, 6249, 6253, 6255, 6563, 6568, 6792, 6806, 6812, 6933, 6936, 6983, 7036, 7288, 7297, 7386, 7608, 7610, 8359, 8360, 8363, 8416, 8417, 8420, 8465, 8466, 8469, 8514, 8515, 8518, 8518, 8518, 8512, 851, 8512, 851, 8512, 8513, 8514, 8515, 8518 %str_seq:NN...... 1061, 1561, 1562, 2511, 2782, 2812, 3917, 3918, 4114, 4142, 4433, 4443, 4462, 4476, 4477, 4751, 4946, 5935, 5948, 5961, 6075, 6139, 6782, 6791, 6841, 6893, 7272, 7353, 7571, 7575, 7599, 7601, 7614, 7628, 7630, 7631, 8293 %str_uppercase:n...... 7866 %l_tmpa_str...... 152, 153, 154, 155, 156, 157, 158, 162, 178, 182, 183, 184, 186, 1891, 1892, 1893, 1898, 1906, 2797, 2800, 2805, 2812 %subparagraph...... 26, 71 %subproof (env.)...... 7272 %subproof...... 7230, 7331 %subproof...... 7272 %subproof...... 7272 %subproof...... 7272 %subsection...... 726, 71 %subsection...... 25, 26, 71 %subsubsection...... 26, 71 %subsection...... 26, 71 %subsection.




