\begin{smodule}[ns=https://github.com/slatex/sTeX/doc]{SymbolsAndNotations}
\begin{sfragment}{Declaring New Symbols and Notations}
  Inside an \stexcode"smodule" environment, we can declare new \sTeX symbols.

\begin{function}{\symdecl}
  The most basic command for doing so is using \stexcode"\symdecl{symbolname}". This
  introduces a new symbol with name |symbolname|, arity $0$ and semantic macro
  \stexcode"\symbolname".

  The starred variant \stexcode"\symdecl*{symbolname}" will declare a symbol, but not
  introduce a semantic macro.  If we don't want to supply a notation (for example to
  introduce concepts like ``abelian'', which is not something that has a notation), the
  starred variant is likely to be what we want.
\end{function}
\begin{mmtbox}
  \stexcode"\symdecl" introduces a new \omdoc/\mmt constant in the current module
  (=\omdoc/\mmt theory).  Correspondingly, they get assigned the URI
  |<module-URI>?<constant-name>|.
\end{mmtbox}

Without a semantic macro or a notation, the only meaningful way to reference a symbol is
via \stexcode"\symref",\stexcode"\symname" etc.

\stexexample{%
\symdecl*{foo}
Given a \symname{foo}, we can...
}

Obviously, most semantic macros should take actual \emph{arguments}, implying that the
symbol we introduce is an \emph{operator} or \emph{function}. We can let
\stexcode"\symdecl" know the \emph{arity} (i.e. number of arguments) of a symbol like
this:

\stexexample{%
\symdecl{binarysymbol}[args=2]
\symref{binarysymbol}{this} is a symbol taking two arguments.
}

So far we have gained exactly \ldots nothing by adding the arity information: we cannot do
anything with the arguments in the text.

We will now see what we can gain with more machinery.
    
\begin{function}{\notation}
  We probably want to supply a notation as well, in which case we can finally actually use
  the semantic macro in math mode.  We can do so using the \stexcode"\notation" command,
  like this:

\stexexample{%
\notation{binarysymbol}{\text{First: }#1\text{; Second: }#2}
$\binarysymbol{a}{b}$ }
\end{function}

\begin{mmtbox}
  Applications of semantic macros, such as \stexcode"\binarysymbol{a}{b}" are translated
  to \mmt/\omdoc as |OMA|-terms with head |<OMS name="...?binarysymbol"/>|.

  Semantic macros with no arguments correspond to |OMS| directly.
\end{mmtbox}

\begin{function}{\comp}
  For many semantic services e.g. semantic highlighting or \defemph{wikification} (linking
  user-visible notation components to the definition of the respective symbol they come
  from), we need to specify the notation components. Unfortunately, there is currently no
  way the \sTeX engine can infer this by itself, so we have to specify it manually in the
  notation specification.  We can do so with the \stexcode"\comp" command.
\end{function}

We can introduce a new notation |highlight| for \stexcode"\binarysymbol" that fixes this
flaw, which we can subsequently use with \stexcode"\binarysymbol[highlight]":

\stexexample{%
\notation{binarysymbol}[highlight]
    {\comp{\text{First: }}#1\comp{\text{; Second: }}#2}
$\binarysymbol[highlight]{a}{b}$
}

\begin{dangerbox}
  Ideally, \stexcode"\comp" would not be necessary: Everything in a notation that is
  \emph{not} an argument should be a notation component. Unfortunately, it is
  computationally expensive to determine where an argument begins and ends, and the
  argument markers |#n| may themselves be nested in other macro applications or
  \TeX\xspace groups, making it ultimately almost impossible to determine them
  automatically while also remaining compatible with arbitrary highlighting customizations
  (such as tooltips, hyperlinks, colors) that users might employ, and that are ultimately
  invoked by \stexcode"\comp".
\end{dangerbox}

\begin{dangerbox}
  Note that it is required that
  \begin{enumerate}
  \item the argument markers |#n| never occur inside a \stexcode"\comp", and
  \item no semantic arguments may ever occur inside a notation.
  \end{enumerate}
  Both criteria are not just required for technical reasons, but conceptionally
  meaningful:
        
  The underlying principle is that the arguments to a semantic macro represent
  \emph{arguments to the mathematical operation} represented by a symbol. For example, a
  semantic macro \stexcode"\addition{a}{b}" taking two arguments would represent \emph{the
    actual addition of (mathematical objects) $a$ and $b$}.  It should therefore be
  impossible for $a$ or $b$ to be part of a notation component of \stexcode"\addition".

  Similarly, a semantic macro can not conceptually be part of the notation of
  \stexcode"\addition", since a semantic macro represents a \emph{distinct mathematical
    concept} with \emph{its own semantics}, whereas notations are syntactic
  representations of the very symbol to which the notation belongs.

  If you want an argument to a semantic macro to be a purely syntactic parameter, then you
  are likely somewhat confused with respect to the distinction between the precise
  \emph{syntax} and \emph{semantics} of the symbol you are trying to declare (which
  happens quite often even to experienced \sTeX users), and might want to give those
  another thought - quite likely, the macro you aim to implement does not actually
  represent a semantically meaningful mathematical concept, and you will want to use
  \stexcode"\def" and similar native \LaTeX\xspace macro definitions rather than semantic
  macros.
\end{dangerbox}

\begin{function}{\symdef}
  In the vast majority of cases where a symbol declaration should come with a semantic
  macro, we will want to supply a notation immediately. For that reason, the
  \stexcode"\symdef" command combines the functionality of both \stexcode"\symdecl" and
  \stexcode"\notation" with the optional arguments of both:
\end{function}

\stexexample{%
\symdef{newbinarysymbol}[hl,args=2]
    {\comp{\text{1.: }}#1\comp{\text{; 2.: }}#2}
$\newbinarysymbol{a}{b}$
}

We just declared a new symbol |newbinarysymbol| with |args=2| and immediately provided it
with a notation with identifier |hl|. Since |hl| is the \emph{first} (and so far, only)
notation supplied for |newbinarysymbol|, using \stexcode"\newbinarysymbol" without
optional argument defaults to this notation.\bigskip

But one man's meat is another man's poison: it is very subjective what the ``default
notation'' of an operator should be. Different communities have different practices. For
instance, the complex unit is written as $i$ in Mathematics and as $j$ in electrical
engineering. So to allow modular specification and facilitate re-use of document fragments
\sTeX allows to re-set notation defaults.

\begin{function}{\setnotation}
  The first notation provided will stay the default notation unless explicitly changed --
  this is enabled by the \stexcode"\setnotation" command:
  \stexcode"\setnotation{symbolname}{notation-id}" sets the default notation of
  \stexcode"\symbolname" to |notation-id|, i.e. henceforth, \stexcode"\symbolname" behaves
  like \stexcode"\symbolname[notation-id]" from now on.
\end{function}

Often, a default notation is set right after the corresponding notation is introduced --
the starred version \stexcode"\notation*" for that reason introduces a new notation and
immediately sets it to be the new default notation. So expressed differently, the
\emph{first} \stexcode"\notation" for a symbol behaves exactly like \stexcode"\notation*",
and \stexcode"\notation*{foo}[bar]{...}" behaves exactly like
\stexcode"\notation{foo}[bar]{...}\setnotation{foo}{bar}".

\begin{function}{\textsymdecl}
  In the less mathematical settings where we want a symbol and
  semantic macro for some concept with a notation \emph{beyond}
  its mere name, but which should also be available in \TeX's text
  mode, the command \stexcode"\textsymdecl" is useful.
  For example, we can declare a symbol \stexcode"openmath"
  with the notation \stexcode"\textsc{OpenMath}" using
  \textsymdecl{openmath}[name=OpenMath]{\textsc{OpenMath}}
  \stexcode"\textsymdecl{openmath}[name=OpenMath]{\textsc{OpenMath}}".
  The \stexcode"\openmath" yields \openmath both in text and math
  mode.
\end{function}
    
\begin{sfragment}{Operator Notations}
  Once we have a semantic macro with arguments, such as \stexcode"\newbinarysymbol", the
  semantic macro represents the \emph{application} of the symbol to a list of
  arguments. What if we want to refer to the operator \emph{itself}, though?

  We can do so by supplying the \stexcode"\notation" (or \stexcode"\symdef") with an
  \emph{operator notation}, indicated with the optional argument |op=|.  We can then
  invoke the operator notation using \stexcode"\symbolname![notation-identifier]".  Since
  operator notations never take arguments, we do not need to use \stexcode"\comp" in it,
  the whole notation is wrapped in a \stexcode"\comp" automatically:

  \stexexample{%
    \notation{newbinarysymbol}[ab, op={\text{a:}\cdot\text{; b:}\cdot}]
    {\comp{\text{a:}}#1\comp{\text{; b:}}#2} \symname{newbinarysymbol} is also
    occasionally written $\newbinarysymbol![ab]$
  }

  \begin{mmtbox}
    \stexcode"\symbolname!" is translated to \omdoc/\mmt as |<OMS name="...?symbolname"/>|
    directly.
  \end{mmtbox}

\end{sfragment}
\end{sfragment}

\begin{sfragment}{Argument Modes}
  The notations so far used \emph{simple} arguments which we call \emph{mode}-|i|
  arguments. Declaring a new symbol with \stexcode"\symdecl{foo}[args=3]" is equivalent to
  writing \stexcode"\symdecl{foo}[args=iii]", indicating that the semantic macro takes
  three mode-|i| arguments. However, there are three more argument modes which we will
  investigate now, namely mode-|b|, mode-|a| and mode-|B| arguments.

\begin{sfragment}{Mode-\texttt b Arguments}

A mode-|b| argument represents a \emph{variable} that is \emph{bound} by the symbol in
its application, making the symbol a \emph{binding operator}. Typical examples of
binding operators are e.g. sums $\sum$, products $\prod$, integrals $\int$, quantifiers
like $\forall$ and $\exists$, that $\lambda$-operator, etc.

\begin{mmtbox}
  Mode-|b| arguments behave exactly like mode-|i| arguments within \TeX, but applications
  of binding operators, i.e. symbols with mode-|b| arguments, are translated to
  |OMBIND|-terms in \omdoc/\mmt, rather than |OMA|.
\end{mmtbox}

For example, we can implement a summation operator binding an index variable and taking
lower and upper index bounds and the expression to sum over like this:

\stexexample{%
\symdef{summation}[args=biii]
  {\mathop{\comp{\sum}}_{#1\comp{=}#2}^{#3}#4}
  $\summation{\svar{x}}{1}{\svar{n}}{\svar{x}}^2$
}

where the variable $\svar{x}$ is now \emph{bound} by the \stexcode"\summation"-symbol in
the expression.
\end{sfragment}
    
\begin{sfragment}{Mode-\texttt a Arguments}
  Mode-|a| arguments represent a \emph{flexary argument sequence}, i.e. a sequence of
  arguments of arbitrary length.  Formally, operators that take arbitrarily many arguments
  don't ``exist'', but in informal mathematics, they are ubiquitous.  Mode-|a| arguments
  allow us to write e.g.  \stexcode"\addition{a,b,c,d,e}" rather than having to write
  something like \stexcode"\addition{a}{\addition{b}{\addition{c}{\addition{d}{e}}}}"!

  \stexcode"\notation" (and consequently \stexcode"\symdef", too) take one additional
  argument for each mode-|a| argument that indicates how to ``accumulate'' a
  comma-separated sequence of arguments. This is best demonstrated on an example.

  Let's say we want an operator representing quantification over an ascending chain of
  elements in some set, i.e.  \stexcode"\ascendingchain{S}{a,b,c,d,e}{t}" should yield
  $\forall a{<_S}b{<_S}c{<_S}d{<_S}e.\,t$. The ``base''-notation for this operator is
  simply\\ \stexcode"{\comp{\forall} #2\comp{.\,}#3}", where |#2| represents the full
  notation fragment \emph{accumulated} from |{a,b,c,d,e}|.
        
  The \emph{additional} argument to \stexcode"\notation" (or \stexcode"\symdef") takes the
  same arguments as the base notation and two \emph{additional} arguments |##1| and |##2|
  representing successive pairs in the mode-|a| argument, and accumulates them into |#2|,
  i.e. to produce $a<_Sb<_Sc<_Sd<_Se$, we do \stexcode"{##1 \comp{<}_{#1} ##2}":

  \stexexample{%
\symdef{ascendingchain}[args=iai]
  {\comp{\forall} #2\comp{.\,}#3}
  {##1 \comp{<}_{#1} ##2}

Tadaa: $\ascendingchain{S}{a,b,c,d,e}{t}$
}

If this seems overkill, keep in mind that you will rarely need the single-hash arguments
|#1|,|#2| etc.  in the |a|-notation-argument.  For a much more representative and simpler
example, we can introduce flexary addition via:
\stexexample{%
  \symdef{addition}[args=a]{#1}{##1 \comp{+} ##2}
  
Tadaa: $\addition{a,b,c,d,e}$
}

\begin{sfragment}{The \texttt{assoc}-key}
  We mentioned earlier that ``formally'', flexary arguments don't really
  ``exist''. Indeed, formally, addition is usually defined as a binary operation,
  quantifiers bind a single variable etc.

  Consequently, we can tell \sTeX (or, rather, \mmt/\omdoc) how to ``resolve'' flexary
  arguments by providing \stexcode"\symdecl" or \stexcode"\symdef" with an optional
  |assoc|-argument, as in \stexcode"\symdecl{addition}[args=a,assoc=bin]".  The possible
  values for the |assoc|-key are:
  \begin{itemize}
  \item[|bin|:] A binary, associative argument, e.g.  as in \stexcode"\addition"
  \item[|binl|:] A binary, left-associative argument, e.g.
    $a^{\scriptstyle b^{\scriptstyle c^d}}$, which stands for $((a^b)^c)^d$
  \item[|binr|:] A binary, right-associative argument, e.g. as in $A\to B\to C\to D$,
    which stands for $A \to (B \to (C \to D))$
  \item[|pre|:] Successively prefixed, e.g. as in $\forall x,y,z.\,P$, which stands for
    $\forall x.\, \forall y.\, \forall z.\,P$
  \item[|conj|:] Conjunctive, e.g. as in $a=b=c=d$ or $a,b,c,d\in A$, which stand for
    $a=d\wedge b=d\wedge c=d$ and $a\in A\wedge b\in A \wedge c\in A\wedge d\in A$,
    respectively
  \item[|pwconj|:] Pairwise conjunctive, e.g. as in $a\neq b\neq c\neq d$, which stands
    for $a\neq b\wedge a\neq c\wedge a\neq d\wedge b\neq c\wedge b\neq d\wedge c\neq d$
  \end{itemize}
  As before, at the PDF level, this annotation is invisible (and without effect), but at
  the level of the generated OMDoc/MMT this leads to more semantical expressions.
\end{sfragment}
\end{sfragment}
    
\begin{sfragment}{Mode-\texttt B Arguments}
  Finally, mode-|B| arguments simply combine the functionality of both |a| and |b| -
  i.e. they represent an arbitrarily long sequence of variables to be bound, e.g. for
  implementing quantifiers:

  \stexexample{%
\symdef{quantforall}[args=Bi]
  {\comp{\forall}#1\comp{.}#2}
  {##1\comp,##2}

$\quantforall{\svar{x},\svar{y},\svar{z}}{P}$
}
\end{sfragment}
\end{sfragment}

\begin{sfragment}{Type and Definiens Components}
  \stexcode"\symdecl" and \stexcode"\symdef" take two more optional arguments. \TeX\xspace
  largely ignores them (except for special situations we will talk about later), but \mmt
  can pick up on them for additional services. These are the |type| and |def| keys, which
  expect expressions in math-mode (ideally using semantic macros, of course!)

  \begin{mmtbox}
    The |type| and |def| keys correspond to the |type| and |definiens| components of
    \omdoc/\mmt constants.

    Correspondingly, the name ``type'' should be taken with a grain of salt, since
    \omdoc/\mmt -- being foundation-independent -- does not a priori implement a fixed
    typing system.
  \end{mmtbox}

  \symdef{funtype}[args=ai]{#1 \comp\to #2}{##1 \comp\times ##2}
  \symdef{fun}[args=bi]{#1 \comp\mapsto #2}
  \symdef{set}{\comp{\texttt{Set}}}
  
  The |type|-key allows us to provide additional information
  (given the necessary \sTeX symbols), e.g. for
  addition on natural numbers:
  
  \stexexample{%
\symdef{Nat}[type=\set]{\comp{\mathbb N}}
\symdef{addition}[
    type=\funtype{\Nat,\Nat}{\Nat},
    op=+,
    args=a
]{#1}{##1 \comp+ ##2}

\symname{addition} is an operation $\funtype{\Nat,\Nat}{\Nat}$
}

The |def|-key allows for declaring symbols as abbreviations:
\stexexample{%
\symdef{successor}[
    type=\funtype{\Nat}{\Nat},
    def=\fun{\svar{x}}{\addition{\svar{x},1}},
    op=\mathtt{succ},
    args=1
]{\comp{\mathtt{succ(}#1\comp{)}}}

The \symname{successor} operation $\funtype{\Nat}{\Nat}$
is defined as $\fun{\svar{x}}{\addition{\svar{x},1}}$
}
\end{sfragment}

\begin{sfragment}{Precedences and Automated Bracketing}
  Having done \stexcode"\addition", the obvious next thing to implement is
  \stexcode"\multiplication".  This is straight-forward in theory:

  \stexexample{%
\symdef{multiplication}[
    type=\funtype{\Nat,\Nat}{\Nat},
    op=\cdot,
    args=a
]{#1}{##1 \comp\cdot ##2}

\symname{multiplication} is an operation $\funtype{\Nat,\Nat}{\Nat}$
}

However, if we \emph{combine} \stexcode"\addition" and \stexcode"\multiplication", we
notice a problem:

\stexexample{%
$\addition{a,\multiplication{b,\addition{c,\multiplication{d,e}}}}$
}

We all know that $\multiplication!$ binds stronger than $\addition!$, so the output
$\addition{a,\multiplication{b,\addition{c,\multiplication{d,e}}}}$ does not actually
reflect the term we wrote. We can of course insert parentheses manually

\stexexample{%
$\addition{a,\multiplication{b,(\addition{c,\multiplication{d,e}})}}$
}
but we can also do better by supplying \emph{precedences} and
have \sTeX insert parentheses automatically.

For that purpose, \stexcode"\notation" (and hence \stexcode"\symdef") take an optional
argument |prec=<opprec>;<argprec1>x...x<argprec n>|.

We will investigate the precise meaning of |<opprec>| and the |<argprec>|s shortly -- in
the vast majority of cases, it is perfectly sufficient to think of |prec=| taking a single
number and having that be \emph{the} precedence of the notation, where lower precedences
(somewhat counterintuitively) bind stronger than higher precedences.  So fixing our
notations for \stexcode"\addition" and \stexcode"\multiplication", we get:

\stexexample{%
\notation{multiplication}[
    op=\cdot,
    prec=50
]{#1}{##1 \comp\cdot ##2}
\notation{addition}[
    op=+,
    prec=100
]{#1}{##1 \comp+ ##2}

$\addition{a,\multiplication{b,\addition{c,\multiplication{d,e}}}}$
}

Note that the precise numbers used for precedences are pretty arbitrary - what matters is
which precedences are higher than which other precedences when used in conjunction.
\begin{variable}{\infprec,\neginfprec}
  It is occasionally useful to have ``infinitely'' high or low precedences to enforce or
  forbid automated bracketing entirely -- for those purposes, \stexcode"\infprec" and
  \stexcode"\neginfprec" exist (which are implemented as the maximal and minimal integer
  values accordingly).
\end{variable}

\begin{dangerbox}
  More precisely, each notation takes
  \begin{enumerate}
  \item One \emph{operator precedence} and
  \item one \emph{argument precedence} for each argument.
  \end{enumerate}
  By default, all precedences are $0$, unless the symbol takes no argument, in which case
  the operator precedence is \stexcode"\neginfprec" (negative infinity). If we only
  provide a single number, this is taken as both the operator precedence and all argument
  precedences.

  \sTeX decides whether to insert parentheses by comparing operator precedences to a
  \emph{downward precedence} $p_d$ with initial value \stexcode"\infprec".  When
  encountering a semantic macro, \sTeX takes the operator precedence $p_{op}$ of the
  notation used and checks whether $p_{op}>p_d$. If so, \sTeX insert parentheses.

  When \sTeX steps into an argument of a semantic macro, it sets $p_d$ to the respective
  argument precedence of the notation used.

  In the example above:
  \begin{enumerate}
  \item \sTeX starts out with $p_d=$\stexcode"\infprec".
  \item \sTeX encounters \stexcode"\addition" with $p_{op}=100$. Since
    $100\not>$\stexcode"\infprec", it inserts no parentheses.
  \item Next, \sTeX encounters the two arguments for \stexcode"\addition".  Both have no
    specifically provided argument precedence, so \sTeX uses $p_d=p_{op}=100$ for both and
    recurses.
  \item Next, \sTeX encounters \stexcode"\multiplication{b,...}", whose notation has
    $p_{op}=50$.
  \item We compare to the current downward precedence $p_d$ set by \stexcode"\addition",
    arriving at $p_{op}=50\not>100=p_d$, so \sTeX again inserts no parentheses.
  \item Since the notation of \stexcode"\multiplication" has no explicitly set argument
    precedences, \sTeX uses the operator precedence for all arguments of
    \stexcode"\multiplication", hence sets $p_d=p_{op}=50$ and recurses.
  \item Next, \sTeX encounters the inner \stexcode"\addition{c,...}" whose notation has
    $p_{op}=100$.
  \item We compare to the current downward precedence $p_d$ set by
    \stexcode"\multiplication", arriving at $p_{op}=100>50=p_d$ -- which finally prompts
    \sTeX to insert parentheses, and we proceed as before.
  \end{enumerate}
\end{dangerbox}
\end{sfragment}

\begin{sfragment}{Variables}
  All symbol and notation declarations require a module with which they are associated,
  hence the commands \stexcode"\symdecl", \stexcode"\notation", \stexcode"\symdef"
  etc. are disabled outside of |smodule|-environments.

  Variables are different -- variables are allowed everywhere, are not exported when the
  current module (if one exists) is imported (via \stexcode"\importmodule" or
  \stexcode"\usemodule") and (also unlike symbol declarations) ``disappear'' at the end of
  the current \TeX\xspace group.

  \begin{function}{\svar}
    So far, we have always used variables using \stexcode"\svar{n}", which marks-up $n$ as
    a variable with name |n|. More generally, \stexcode"\svar[foo]{<texcode>}" marks-up
    the arbitrary |<texcode>| as representing a variable with name |foo|.
  \end{function}

  Of course, this makes it difficult to reuse variables, or introduce ``functional''
  variables with arities $>0$, or provide them with a type or definiens.

  \begin{function}{\vardef}
    For that, we can use the \stexcode"\vardef" command. Its syntax is largely the same as
    that of \stexcode"\symdef", but unlike symbols, variables have only one notation
    (\textcolor{red}{TODO: so far?}), hence there is only \stexcode"\vardef" and no
    \stexcode"\vardecl".
  \end{function}

\stexexample{%
\vardef{varf}[
    name=f,
    type=\funtype{\Nat}{\Nat},
    op=f,
    args=1,
    prec=0;\neginfprec
]{\comp{f}#1}
\vardef{varn}[name=n,type=\Nat]{\comp{n}}
\vardef{varx}[name=x,type=\Nat]{\comp{x}}

Given a function $\varf!:\funtype{\Nat}{\Nat}$, 
by $\addition{\varf!,\varn}$ we mean the function
$\fun{\varx}{\varf{\addition{\varx,\varn}}}$
}

(of course, ``lifting'' addition in the way described in the previous example is an
operation that deserves its own symbol rather than abusing \stexcode"\addition",
but... well.)

\textcolor{red}{TODO: bind=forall/exists}
\end{sfragment}

\begin{sfragment}{Variable Sequences}
  Variable \emph{sequences} occur quite frequently in informal mathematics, hence they
  deserve special support. Variable sequences behave like variables in that they disappear
  at the end of the current \TeX\xspace group and are not exported from modules, but their
  declaration is quite different.

  \begin{function}{\varseq}
    A variable sequence is introduced via the command \stexcode"\varseq", which takes the
    usual optional arguments |name| and |type|. It then takes a starting index, an end
    index and a \emph{notation} for the individual elements of the sequence parametric in
    an index. Note that both the starting as well as the ending index may be variables.
  \end{function}

  This is best shown by example:
  \stexexample{%
\vardef{varn}[name=n,type=\Nat]{\comp{n}}
\varseq{seqa}[name=a,type=\Nat]{1}{\varn}{\comp{a}_{#1}}

The $i$th index of $\seqa!$ is $\seqa{i}$.
}

Note that the syntax |\seqa!| now automatically generates a presentation based on the
starting and ending index.
        
\textcolor{red}{TODO: more notations for invoking sequences}.

\vardef{varn}[name=n,type=\Nat]{\comp{n}}
\varseq{seqa}[name=a]{1}{\varn}{\comp{a}_{#1}}

Notably, variable sequences are nicely compatible with |a|-type arguments, so we can do
the following:

\stexexample{%
$\addition{\seqa}$
}

Sequences can be \emph{multidimensional} using the |args|-key, in which case the
notation's arity increases and starting and ending indices have to be provided as a
comma-separated list:

\stexexample{%
\vardef{varm}[name=m,type=\Nat]{\comp{m}}
\varseq{seqa}[
    name=a,
    args=2,
    type=\Nat,
]{1,1}{\varn,\varm}{\comp{a}_{#1}^{#2}}

$\seqa!$ and $\addition{\seqa}$
}
\vardef{varm}[name=m,type=\Nat]{\comp{m}}

We can also explicitly provide a ``middle'' segment to be used, like such:

\stexexample{%
\varseq{seqa}[
    name=a,
    type=\Nat,
    args=2,
    mid={\comp{a}_{\varn}^1,\comp{a}_1^2,\ellipses,\comp{a}_{1}^{\varm}}
]{1,1}{\varn,\varm}{\comp{a}_{#1}^{#2}}

$\seqa!$ and $\addition{\seqa}$
}
\end{sfragment}
\end{smodule}

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

%  LocalWords:  binarysymbol newbinarysymbol hl,args a,b,c,d,e ascendingchain assoc binl
%  LocalWords:  a,assoc binr x,y,z conj a,b,c,d pwconj funtype succ prec opprec argprec1
%  LocalWords:  argprec texcode varf varn n,type varx x,type varseq seqa a,type th m,type
