path: root/Master/texmf-dist/doc/latex/stex/stex-manual.tex

\makeatletter
\ifcsname if@infulldoc\endcsname\else
    \expandafter\newif\csname if@infulldoc\endcsname\@infulldocfalse
\fi
\makeatother

\csname if@infulldoc\endcsname\else

\def\bibfolder{../lib/bib}

\input{stex-docheader}

\infulldoctrue

\csname bool_set_true:N\expandafter\endcsname\csname stex_dtx_tests_bool\endcsname

\begin{document}
  \csname if@infulldoc\endcsname\else
	\title{
		The {\stex{3}} Manual
		\thanks{Version {\fileversion} (last revised {\filedate})}
 	}
	\author{Michael Kohlhase, Dennis Müller\\
		FAU Erlangen-Nürnberg\\
		\url{http://kwarc.info/}
	}
	\pagenumbering{roman}
	\maketitle
	
	\input{stex-abstract}\bigskip

  This is the user manual for the \sTeX package and 
  associated software. It is primarily directed at end-users 
  who want to use \sTeX to author semantically
  enriched documents. For the full documentation, see
  \href{\basedocurl/stex.pdf}{the \sTeX documentation}
	
	\makeatletter
		\renewcommand\part{%
    		\clearpage
  			\thispagestyle{plain}%
  			\@tempswafalse
  			\null\vfil
  			\secdef\@part\@spart%
  		}
		\newcounter{chapter}
		\numberwithin{section}{chapter}
		\renewcommand\thechapter{\@arabic\c@chapter}
		\renewcommand\thesection{\thechapter.\@arabic\c@section}
		\newcommand*\chaptermark[1]{}
		\setcounter{secnumdepth}{2}
		\newcommand\@chapapp{\chaptername}
		%\newcommand\chaptername{Chapter}
  		\def\ps@headings{%
    		\let\@oddfoot\@empty
    		\def\@oddhead{{\slshape\rightmark}\hfil\thepage}%
    		\let\@mkboth\markboth
    		\def\chaptermark##1{%
      			\markright{\MakeUppercase{%
        			\ifnum \c@secnumdepth >\m@ne
            			\@chapapp\ \thechapter. \ %
        			\fi
        		##1}}%
        	}%
        }
		\newcommand\chapter{\clearpage
			\thispagestyle{plain}%
			\global\@topnum\z@
			\@afterindentfalse
			\secdef\@chapter\@schapter%
		}
		\def\@chapter[#1]#2{\refstepcounter{chapter}%
			\typeout{\@chapapp\space\thechapter.}%
			\addcontentsline{toc}{chapter}%
				{\protect\numberline{\thechapter}#1}%
			\chaptermark{#1}%
			\addtocontents{lof}{\protect\addvspace{10\p@}}%
			\addtocontents{lot}{\protect\addvspace{10\p@}}%
			\@makechapterhead{#2}%
			\@afterheading%
		}
		\def\@makechapterhead#1{%
			\vspace*{50\p@}%
			{\parindent \z@ \raggedright \normalfont
				\huge\bfseries \@chapapp\space \thechapter
				\par\nobreak
				\vskip 20\p@
				\interlinepenalty\@M
				\Huge \bfseries #1\par\nobreak
				\vskip 40\p@
			}%
		}
\newcommand*\l@chapter[2]{%
  \ifnum \c@tocdepth >\m@ne
    \addpenalty{-\@highpenalty}%
    \vskip 1.0em \@plus\p@
    \setlength\@tempdima{1.5em}%
    \begingroup
      \parindent \z@ \rightskip \@pnumwidth
      \parfillskip -\@pnumwidth
      \leavevmode \bfseries
      \advance\leftskip\@tempdima
      \hskip -\leftskip
      #1\nobreak\hfil
      \nobreak\hb@xt@\@pnumwidth{\hss #2%
                                 \kern-\p@\kern\p@}\par
      \penalty\@highpenalty
    \endgroup
  \fi}
\renewcommand*\l@section{\@dottedtocline{1}{1.5em}{2.8em}}
\renewcommand*\l@subsection{\@dottedtocline{2}{3.8em}{3.2em}}
\renewcommand*\l@subsubsection{\@dottedtocline{3}{7.0em}{4.1em}}
\def\partname{Part}
\def\toclevel@part{-1}
\def\maketitle{\chapter{\@title}}
\let\thanks\@gobble
\let\DelayPrintIndex\PrintIndex
\let\PrintIndex\@empty
\providecommand*{\hexnum}[1]{\text{\texttt{\char`\"}#1}}
\makeatother

\ExplSyntaxOn
\int_set:Nn \l_document_structure_section_level_int {1}
\ExplSyntaxOff

\clearpage

{%
  \def\\{:}% fix "newlines" in the ToC
  \tableofcontents
}

\clearpage
\pagenumbering{arabic}
	
\fi

\long\def\ignore#1{}

\begin{sfragment}{What is \sTeX?}
  
Formal systems for mathematics (such as interactive theorem provers)
have the potential to significantly increase both the accessibility
of published knowledge, as well as the confidence in its veracity,
by rendering the precise semantics of statements machine actionable.
This allows for a plurality of added-value services, from semantic
search up to verification and automated theorem proving.
Unfortunately, their usefulness is hidden behind severe barriers
to accessibility; primarily related to their surface languages
reminiscent of programming languages and very unlike informal
standards of presentation.

\sTeX minimizes this gap between informal and formal 
mathematics by integrating formal methods into established
and widespread authoring workflows, primarily \LaTeX, via 
non-intrusive semantic
annotations of arbitrary informal document fragments. That way
formal knowledge management services become available for informal
documents, accessible via an IDE for authors and via generated
\emph{active} documents for readers, while remaining fully compatible
with existing authoring workflows and publishing systems.

Additionally, an extensible library of reusable
document fragments is being developed, that serve as reference targets
for global disambiguation, intermediaries for content exchange
between systems and other services.

Every component of the system is designed modularly and extensibly,
and thus lay the groundwork for a potential full integration of
interactive theorem proving systems into established informal document
authoring workflows.

\paragraph{} The general \sTeX workflow combines functionalities
provided by several pieces of software:
\begin{itemize}
  \item The \sTeX package to use semantic annotations in
    {\LaTeX} documents,
  \item \RusTeX to convert |tex| sources to (semantically enriched)
    |xhtml|,
  \item The \mmt software, that extracts semantic information
    from the thus generated |xhtml| and provides semantically informed
    added value services.
\end{itemize}


% ----------------------------

\ignore{The objectives of this project will be achieved by developing a 
language and system 
that uses non-intrusive annotations
to augment informal documents with semantic information
(ranging from \textbf{fully formal} to \textbf{purely informal})
 without
impacting linguistic presentation or document layout. 
That way, the system
remains compatible with established publishing
pipelines and practices, while additionally providing flexiformal 
information that
enables formal knowledge management services, and hence produces 
\emph{rich active documents}, satisfying \textbf{R3}, \textbf{R4} and 
\textbf{R5}.
In particular, it will avoid commitment to a fixed logical foundation.
Instead, it will be designed as a modular pipeline of consecutive
and compositional
annotations, semantics extraction and translation steps, extensible
via new structuring mechanisms (\textbf{R1}), library content 
(\textbf{R2}),
NLP techniques, foundations, translation methods and 
end-user services.

Naturally, the benefits of formal knowledge management services scale 
with the amount of mathematics involved. Consequently I will primarily 
focus on those 
STEM fields in which mathematical methods are most prominently
used (e.g. mathematics, physics, computer science). Since in those fields
\LaTeX~is the most commonly used scientific writing tool, I will also
primarily focus on \LaTeX~as a development and evaluation target, but 
the system will be designed such that all components apart from
the surface language will be integrable with other writing tools 
(e.g. WYSIWYG word processors).

\paragraph{} The basic architecture of the proposed system is sketched in
\autoref{fig:architecture}.
\begin{figure}\centering
  \resizebox{0.95\textwidth}{!}{\tikzinput[]{diagram}}
  {\small (Note, that the syntax used
    in the box on the top right is prototypical and subject to change during the project.
    Details and open questions regarding the syntax are discussed here:
    \url{https://github.com/KWARC/FoMID/issues/1})}
  \caption{Basic Architecture of the Proposed System}\label{fig:architecture}
\end{figure}
A user can write their content using standard \LaTeX\ in an IDE;
ideally using semantic annotations provided by \sTeX
%and the library developed in \OBJref{smglom}
(as in the upper right of 
\autoref{fig:architecture}), but not necessarily so.

The document is converted to xhtml with \omdoc annotations
using \LaTeX ML in the background,
thus becoming actionable by the \mmt system. Both the source document
as well as the generated xhtml/\omdoc are accessible to a natural language
processing pripeline that can supply additional inferred semantic 
information or suggest annotations to the user, in the latter case 
augmenting the source document directly. This pipeline can use both 
classical NLP techniques using the GLIF system, as well as machine 
learning models such as \cite{own:fifom}.

A semiformal fragment is converted 
into an appropriate syntax tree (possibly containing opaque
informal nodes), 
thus becoming amenable
to flexiformal knowledge management services. In a consecutive step
-- if sufficiently annotated --, these are
additionally translated
to a fully formal foundation, e.g. using the techniques from 
\cite{DMueller:phd:19,own:translations}, allowing
more powerful services and conversion to established formal
systems. All three representations
are thus available from within the \mmt system for various
knowledge management services, interfaces for which can be
implemented in the IDE.

Importantly, every non-trivial arrow in the figure is 
composable and extensible -- 
translations to a foundation can be provided
by supplying an appropriate formalization and alignment-based
translations (or entirely new methods),
services can be implemented generically using the \mmt API,
NLP techniques can be implemented both inside and alongside of
GLIF, and the concrete syntax within \sTeX can be extended
by convenience macros in \LaTeX\ (enabling new
structuring mechanisms as in \textbf{R1} via 
\mmt extensions, see
\cite{MueRabRot:rslffml20}) as well as via additions to
the library, which will be extensible both from within the IDE
as well as on MathHub,
remaining backwards compatible with existing content in a surface 
language. Additionally, sufficiently disambiguated
statements can be translated to the syntax of 
external systems (such as interactive theorem prover systems
or computer algebra systems),
which can thus be integrated as additional services into the system.
}

\end{sfragment}

\begin{sfragment}{Quickstart}

	\begin{sfragment}{Setup}
		\begin{sfragment}{The \sTeX IDE}
      TODO: VSCode Plugin
    \end{sfragment}
    \begin{sfragment}{Manual Setup}
      Foregoing on the \sTeX IDE, we will need several
      pieces of software; namely:
      \begin{itemize}
        \item \textbf{The \sTeX-Package} available 
          \href{https://github.com/slatex/sTeX/blob/latex3/doc/stex.pdf}{here}%
          \ednote{For now, we require the \texttt{latex3}-branch}.
          Note, that the CTAN repository for \LaTeX{} packages
          may contain outdated versions of the \sTeX package, so
          make sure, that your |TEXMF| system variable is configured such
          that the packages available in the linked repository are prioritized
          over potential default packages that come with your \TeX{} distribution.

          %If you are only interested in using semantic macros in (ultimately)
          %|pdf|s generated by |pdflatex|, this is all you need.

        \item \textbf{The \mmt System} available
          \href{https://github.com/uniformal/MMT/tree/sTeX}{here}%
          \ednote{For now, we require the \texttt{sTeX}-branch, requiring manually
          compiling the MMT sources}. We recommend following
          the setup routine documented 
          \href{https://uniformal.github.io//doc/setup/}{here}.

          Following the setup routine (Step 3) will entail designating
          a |MathHub|-directory on your local file system, where
          the \mmt system will look for \sTeX/\mmt content archives.

        \item To make sure that \sTeX too knows where to find its
          archives, we need to set a global system variable |MATHHUB|,
          that points to your local |MathHub|-directory 
          (see \sref{sec.stexarchives}).
        \item \textbf{\sTeX Archives} If we only care about {\LaTeX} and generating |pdf|s, we do not
          technically need \mmt at all; however, we still need the |MATHHUB|
          system variable to be set. Furthermore, \mmt can make downloading
          content archives we might want to use significantly easier, since
          it makes sure that all dependencies of (often highly interrelated)
          \sTeX archives are cloned as well.

          Once set up, we can run |mmt| in a shell and download an archive along with
          all of its dependencies like this: |lmh install <name-of-repository>|,
          or a whole \emph{group} of archives; for example,
          |lmh install smglom| will download all smglom archives.
        \item \textbf{\RusTeX} The \mmt system will also set up \RusTeX for you,
          which is used to generate (semantically annotated)
          |xhtml| from tex sources. In lieu of using \mmt, you
          can also download and use \RusTeX directly
          \href{https://github.com/slatex/RusTeX}{here}.

      \end{itemize}
    \end{sfragment}
	\end{sfragment}
	\begin{sfragment}{A First \sTeX Document}
    Having set everything up, we can write a first
    \sTeX document. As an example, we will use the
    |smglom/calculus| and |smglom/arithmetics| archives, 
    which should be present in the designated |MathHub|-folder.

    The document we will consider is the following:
    \begin{framed}\begin{latexcode}
\documentclass{article}
\usepackage{stex}
\usepackage{xcolor}
\def\compemph#1{\textcolor{blue}{#1}}

\begin{document}
  \usemodule[smglom/calculus]{series}
  \usemodule[smglom/arithmetics]{realarith}

  The \symref{series}{series} $\infinitesum{n}{1}{
    \realdivide[frac]{1}{
      \realpower{2}{n}
    }
  }$ \symref{converges}{converges} towards $1$.
    
\end{document}
    \end{latexcode}\end{framed}

    Compiling this document with |pdflatex| should yield
    the output

    \begin{framed}
        The \textbf{series} 
        $\textcolor{blue}{\sum}_{n=1}^{\textcolor{blue}\infty} \frac{1}{2^n}$
        \textbf{converges} towards $1$.
    \end{framed}

    Note that the $\sum$ and $\infty$-symbols are highlighted in blue,
    and the words ``series'' and ``converges'' in bold.
    This signifies that these words and symbols 
    reference \sTeX \emph{symbols}
    formally declared somewhere; associating their 
    \emph{presentation} in the document with their (formal)
    definition - i.e. their semantics. The precise way
    in which they are highlighted (if at all) can of course
    be customized (see \ednote{somewhere later}).

    \begin{function}{\usemodule}
      The command |\usemodule[some/archive]{modulename}|
      finds some module in the appropriate archive -- in the first
      case (|\usemodule[smglom/calculus]{series}|), \sTeX
      looks for the archive |smglom/calculus| in our local
      MathHub-directory (see \sref{sec.stexarchives}), and
      in its source-folder for a file |series.tex|. Since no such
      file exists, and by default the document is assumed to be
      in \emph{english}, it picks the file |series.en.tex|, and
      indeed, in here we find a statement |\begin{smodule}{series}|.
      \iffalse\end{smodule}\fi
      
      \sTeX now reads this file and makes all semantic macros therein
      available to use, along with all its dependencies.
      This enables the usage of |\infinitesum| later on.

      Analogously, |\usemodule[smglom/arithmetics]{realarith}|
      opens the file |realarith.en.tex| in the |.../smglom/arithmetics/source|-folder
      and makes its contents available, e.g. |\realdivide| and |\realpower|.
    \end{function}

    \begin{function}{\symref,\symname}
      The command |\symref{symbolname}{text}| marks the |text|
      in the second argument as representing the |symbolname|
      in the first argument -- which is why the word ``series''
      is set in boldface. In the pdf, this is all that happens.
      In the |xhtml| (which we will investigate shortly) however,
      we will note that the word ``series'' is now annotated with the
      full URI of the symbol denoting the \emph{mathematical concept of
      a series}. In other words, the word is associated with an unambiguous
      semantics.

      Notably, in both cases above (\emph{series} and \emph{converges})
      the text that \emph{references} the symbol and the name of the symbol
      are identical. Since this occurs quite often, the shorthand
      |\symname{converges}| would have worked as well, where
      |\symname{foo-bar}| behaves exactly like |\symref{foo-bar}{foo bar}|
      - i.e. the text is simply the name of the symbol with ``|-|'' replaced by
      a space.
    \end{function}

    \begin{function}{\importmodule}
      If you investigated the contents of the imported modules 
      (|realarith| and |series|) more closely, you'll note that
      none of them contain a symbol ``|converges|''. Yet, we
      can use |\symref| to refer to ``converges''. That is because
      the symbol |converges| is found in 
      |smglom/calculus/source/sequenceConvergence.en.tex|, and
      |series.en.tex| contains the line
      |\importmodule{sequenceConvergence}|. The |\importmodule|-statement
      makes the module referenced available to all documents
      that include the current module. As such, a ``current module''
      has to exist for |\importmodule| to work, which is why the command
      is only allowed within a |module|-environment.
    \end{function}

    \textcolor{red}{TODO} explain |xhtml| conversion, MMT compilation
    (requires an archive...?).

	\end{sfragment}
\end{sfragment}

\begin{sfragment}{Using \sTeX}
  \input{packages/stex-basics}
  
  \input{packages/stex-terms}

  \input{packages/stex-references}
\end{sfragment}

\begin{sfragment}[id=sec.stexarchives]{\sTeX Archives}
  \input{packages/stex-mathhub}
\end{sfragment}

\begin{sfragment}{Creating New Modules and Symbols}
	\textcolor{red}{TODO}

  \stexexample{
    \begin{smodule}{assoctest}
      \symdef{foo}[args=iia]{\comp{a:}#1\comp{;b:}#2\comp{;c:}#3}{\comp[#1\comp{;}##1\comp+##2\comp;#2\comp]}
      $\foo {w_1}{w_2}{x,y,z}$
    \end{smodule}
   }
   
  \input{packages/stex-modules}

  \input{packages/stex-symbols}

  \input{packages/stex-inheritance}

  \begin{sfragment}{Advanced Structuring Mechanisms}
    \input{packages/stex-features}
  \end{sfragment}
  \begin{sfragment}{Primitive Symbols (The \sTeX Metatheory)}
    \input{packages/stex-metatheory}
  \end{sfragment}
\end{sfragment}

\begin{sfragment}{\sTeX Statements (Definitions, Theorems, Examples, ...)}
  \input{packages/stex-statements}

  \input{packages/stex-proofs}
\end{sfragment}

\begin{sfragment}{Additional Packages}
  \input{packages/stex-tikzinput}
  \begin{sfragment}{Modular Document Structuring}
    \input{packages/stex-document-structure}
  \end{sfragment}
  \begin{sfragment}{Slides and Course Notes}
    \input{packages/stex-slides}
  \end{sfragment}
  \begin{sfragment}{Homework, Problems and Exams}
    \input{packages/stex-problem}
    
    \input{packages/stex-hwexam}
  \end{sfragment}

\end{sfragment}

\chapter{Stuff}

\section{Modules}


\begin{function}{\sTeX , \stex}
  Both print this \stex logo.
\end{function}

 \subsection{Semantic Macros and Notations}

 Semantic macros invoke a formally declared symbol.

 To declare a symbol (in a module), we use \cs{symdecl},
 which takes as argument the name of the corresponding
 semantic macro, e.g. |\symdecl{foo}| introduces the macro
 \cs{foo}. Additionally, \cs{symdecl} takes several options,
 the most important one being its arity. |foo| as declared above
 yields a \emph{constant} symbol. To introduce an \emph{operator}
 which takes arguments, we have to specify which arguments it takes.

 \begin{smodule}{SemanticMacrosExample}
   For example, to introduce binary multiplication,
   we can do |\symdecl{mult}[args=2]|. We can then supply
   the semantic macro with arbitrarily many notations, such as
   |\notation{mult}{#1 #2}|.
   
   \stexexample{
 \symdecl{mult}[args=2]
 \notation{mult}{#1 #2}
 $\mult{a}{b}$
}

 Since usually, a freshly introduced symbol also comes with a
 notation from the start, the \cs{symdef} command combines
 \cs{symdecl} and \cs{notation}. So instead of the above,
 we could have also written
 \begin{center} |\symdef{mult}[args=2]{#1 #2}| \end{center}

 \symdecl{mult}[args=2]
 \notation{mult}{#1 #2}

   \notation{mult}[cdot]{#1 \comp{\cdot} #2}
   \notation{mult}[times]{#1 \comp{\times} #2}
   Adding more notations like
   |\notation{mult}[cdot]{#1 \comp{\cdot} #2}| or 
   |\notation{mult}[times]{#1 \comp{\times} #2}|
   allows us to write |$\mult[cdot]{a}{b}$| and
   |$\mult[times]{a}{b}$|:
   \stexexample{
   \notation{mult}[cdot]{#1 \comp{\cdot} #2}
   \notation{mult}[times]{#1 \comp{\times} #2}
 $\mult[cdot]{a}{b}$ and $\mult[times]{a}{b}$
}
   \notation{mult}[cdot]{#1 \comp{\cdot} #2}
   \notation{mult}[times]{#1 \comp{\times} #2}

   Not using an explicit option with a semantic macro yields
   the first declared notation, unless changed\ednote{TODO}.

   Outside of math mode, or by using the starred variant
   |\foo*|, allows to provide a custom notation, where
   notational (or textual) components can be given
   explicitly in square brackets.
   \stexexample{
 $\mult*{\arg{a}\comp{\ast}\arg{b}}$ is the 
 \mult{\comp{product of} \arg{$a$} \comp{and} \arg{$b$}}
}

   In custom mode, prefixing an argument with a star will not
   print that argument, but still export it to \omdoc:
   \stexexample{
 \mult{\comp{Multiplying} \arg*{$\mult{a}{b}$} again by \arg{$b$}} yields...
}
   The syntax |*[|\meta{int}|]| allows switching
   the order of arguments. For example, given a 2-ary semantic
   macro |\forevery| with exemplary notation
   |\forall #1. #2|, we can write
   \stexexample{
     \symdecl{forevery}[args=2]
     \forevery{\arg[2]{The proposition $P$} \comp{holds for every} \arg[1]{$x\in A$}}
}

 When using |*[|$n$|]|, after reading the provided ($n$th) argument,
  the ``argument counter'' automatically 
 continues where we left off, so the |*[1]| in the above example
 can be omitted.

   For a macro with arity $>0$, we can refer to the operator
   \emph{itself} semantically by suffixing the semantic macro
   with an exclamation point |!| in either text or math mode.
   For that reason \cs{notation} (and thus \cs{symdef}) take an
   additional optional argument |op=|, which allows to assign
   a notation for the operator itself. e.g.
   \stexexample{
     \symdef{add}[args=2,op={+}]{#1 \comp+ #2}
     The operator $\add!$ adds two elements, as in $\add ab$.
   }

  |*| is composable with |!| for custom notations, as in:

   \stexexample{
 \mult!{\comp{Multiplication}} (denoted by $\mult!*{\comp\cdot}$) is defined by...
}

 The macro \cs{comp} as used everywhere above is responsible
 for highlighting, linking, and tooltips, and should be wrapped
 around the notation (or text) components that should be treated
 accordingly. While it is attractive to just wrap a whole notation,
 this would also wrap around e.g. the arguments themselves, so
 instead, the user is tasked with marking the notation components
 themself.

 The precise behaviour of \cs{comp} is governed by
 the macro \cs{@comp}, which takes two arguments: The tex code
 of the text
 (unexpanded) to highlight, and the URI of the current symbol.
 \cs{@comp} can be safely redefined to customize the behaviour.


 The starred variant |\symdecl*{foo}| does not introduce a semantic
 macro, but still declares a corresponding symbol. |foo| (like
 any other symbol, for that matter) can
 then be accessed via \cs{STEXsymbol}|{foo}| or (if |foo| was declared
 in a module |Foo|) via \cs{STEXModule}|{Foo}?{foo}|.

 both \cs{STEXsymbol} and \cs{STEXModule} take any
 arbitrary ending segment of a full URI to determine
 which symbol or module is meant. e.g.
 \cs{STEXsymbol}|{Foo?foo}| is also valid, as are e.g.
 \cs{STEXModule}|{path?Foo}?{foo}| or
 \cs{STEXsymbol}|{path?Foo?foo}|

 There's also a convient shortcut \cs{symref}|{?foo}{some text}| for
 \cs{STEXsymbol}|{?foo}![some text]|.

 \end{smodule}

 \subsubsection{Other Argument Types}

 So far, we have stated the arity of a semantic macro directly.
 This works if we only have ``normal'' (or more precisely: |i|-type) arguments.
  To make use of other argument types, instead of providing the arity
 numerically, we can provide it as a sequence of characters representing
 the argument types -- e.g. instead of writing |args=2|, we
 can equivalently write |args=ii|, indicating that the macro
 takes two |i|-type arguments.

 Besides |i|-type arguments, \sTeX has two other types, which we will
 discuss now.

 The first are \emph{binding} (|b|-type) arguments, representing
 variables that are \emph{bound} by the operator. This is the
 case for example in the above \cs{forevery}-macro:
 The first argument is not actually an argument that the
 |forevery| ``function'' is ``applied'' to; rather, the first argument
 is a new variable (e.g. $x$) that is \emph{bound} in the subsequent
 argument. More accurately, the macro should therefore have been
 implemented thusly:
   \begin{center}|\symdef{forevery}[args=bi]{\forall #1.\; #2}|\end{center}

 \begin{smodule}{OtherArgs}
 |b|-type arguments are indistinguishable from |i|-type arguments
 within \sTeX, but are treated very differently in \omdoc and by \mmt.
 More interesting \emph{within} \sTeX are |a|-type arguments,
 which represent (associative) arguments of flexible arity, which are
 provided as comma-separated lists.
 This allows e.g. better representing the \cs{mult}-macro above:
 
   \stexexample{
 \symdef{mult}[args=a]{#1}{##1 \comp\cdot ##2}
 $\mult{a,b,c,{d^e},f}$
}
 As the example above shows, notations get a little more complicated
 for associative arguments. For every |a|-type argument, the
 \cs{notation}-macro takes an additional argument that declares
 how individual entries in an |a|-type argument list are aggregated.
 The first notation argument then describes how the aggregated
 expression is combined into the full representation.

 For a more interesting example, consider a flexary operator
 for ordered sequences in ordered set, that taking 
 arguments |{a,b,c}| and |\mathbb{R}| prints
 $a \leq b \leq c\in \mathbb R$. This operator takes
 two arguments (an |a|-type argument and an |i|-type argument),
 aggregates the individuals of the associative argument using |\leq|,
 and combines the result with |\in| and the second argument thusly:

   \stexexample{
 \symdef{numseq}[args=ai]{#1 \comp\in #2}{##1 \comp\leq ##2}
 $\numseq{a,b,c}{\mathbb R}$
}

 Finally, |B|-type arguments combine the functionalities of |a|
 and |b|, i.e. they represent flexary binding operator arguments.

\ednote{what about e.g. \detokenize{\int_x\int_y\int_z f dx dy dz}?}
\ednote{``decompose'' a-type arguments into fixed-arity operators?}

 \end{smodule}

 \subsubsection{Precedences}

 Every notation has an (upwards) \emph{operator precedence} and
 for each argument a (downwards) \emph{argument precedence}
 used for automated bracketing. For example, a notation
 for a binary operator \cs{foo} could be declared like this:
 \begin{center} |\notation{foo}[prec=200;500x600]{#1 \comp{+} #2}| \end{center}
 assigning an operator precedence of 200, an argument precedence
 of 500 for the first argument, and an argument precedence of 600
 for the second argument.

 \sTeX insert brackets thusly: Upon encountering a semantic
 macro (such as \cs{foo}), its operator precedence (e.g. 200)
 is compared to the current downwards precedence (initially 
 \cs{neginfprec}). If the operator precedence is \emph{larger}
 than the current downwards precedence, parentheses are inserted
 around the semantic macro.

 Notations for symbols of arity 0 have a default precedence of \cs{infprec},
 i.e. by default, parentheses are never inserted around constants.
 Notations for symbols with arity $>0$ have a default operator
 precedence of $0$.
 If no argument precedences are explicitly provided, then by
 default they are equal to the operator precedence.

 Consequently, if some operator $A$ should bind stronger than
 some operator $B$, then $A$s operator precedence should be
 smaller than $B$s argument precedences.

 For example:
 \begin{smodule}{NotationsEx}
 \symdecl{plus}[args=2]
 \symdecl{times}[args=2]
 \stexexample{
\notation{plus}[prec=100]{#1 \comp{+} #2}
\notation{times}[prec=50]{#1 \comp{\cdot} #2}
$\plus{a}{\times{b}{c}}$ and $\times{a}{\plus{b}{c}}$
}


 \end{smodule}

 \subsection{Archives and Imports}

 \subsubsection{Namespaces}
   Ideally, \sTeX would use arbitrary URIs for modules, with no
   forced relationships between the \emph{logical} namespace
   of a module and the \emph{physical} location of the file
   declaring the module -- like \mmt does things.

   Unfortunately, \TeX\ 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:

   \begin{itemize}
     \item If \cs{begin}|{module}{Foo}| occurs in a file
       |/path/to/file/Foo[.|\meta{lang}|].tex| which does not belong
       to an archive, the namespace is |file://path/to/file|.
     \item If the same statement occurs in a file
       |/path/to/file/bar[.|\meta{lang}|].tex|, the namespace is 
       |file://path/to/file/bar|.
   \end{itemize}

   In other words: outside of 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^^A
   \footnote{which is internally attached to the module name instead,
   but a user need not worry about that.}.

   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|-folder is replaced by the archive's namespace URI.

 \subsubsection{Paths in Import-Statements}

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

 \begin{itemize}
   \item \cs{importmodule}|{Foo}| outside of an archive refers 
     to module |Foo| in the current namespace. Consequently, |Foo|
     must have been declared earlier in the same document or, if not,
     in a file |Foo[.|\meta{lang}|].tex| in the same directory.
   \item The same statement \emph{within} an archive refers to either
     the module |Foo| declared earlier in the same document, 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 |Foo[.|\meta{lang}|].tex|
     directly in the archive's |source|-folder.
   \item Similarly, in \cs{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|-folder,
     respectively.

     The module |Foo| must either be declared in the file
     \meta{top-directory}|/some/path/Foo[.|\meta{lang}|].tex|, or in
     \meta{top-directory}|/some/path[.|\meta{lang}|].tex| (which are
     checked in that order).
   \item Similarly, \cs{importmodule}|[Some/Archive]{some/path?Foo}|
     is resolved like the previous cases, but relative to the archive
     |Some/Archive| in the mathhub-directory.
   \item Finally, \cs{importmodule}|{full://uri?Foo}| naturally refers to the
     module |Foo| in the namespace |full://uri|. Since the file this module
     is declared in can not be determined directly from the URI, the module
     must be in memory already, e.g. by being referenced earlier in the
     same document.

     Since this is less compatible with a modular development, using full
     URIs directly is discouraged.

 \end{itemize} 


	
	
\csname if@infulldoc\endcsname\else\end{document}\fi