\(
% cbs-katex.sty
%
\newcommand{\STYLE}[2]{\htmlClass{cbs-#1}{#2}}
\newcommand{\DECL}[3]{\htmlId{#1:#2}{#3}}
\newcommand{\REF}[3]{\href{###1:#2}{#3}}
\newcommand{\HYPER}[5]{\href{#1/#2/index.html###3:#4}{#5}}
% \SHADE{MATH} can be defined to produce a shaded background to highlight
% inline MATH in running text:
\newcommand{\SHADE}[1]{#1}
% \KEY{TEXT}, \STRING{TEXT}, \ATOM{TEXT}, \LEX{TEXT} can be used in math mode:
\newcommand{\KEY}[1]{\textsf{\textit{\STYLE{Key}{#1}}}}
\newcommand{\STRING}[1]{\textsf{``\texttt{#1}''}}
\newcommand{\ATOM}[1]{\textsf{`\texttt{#1}'}}
\newcommand{\LEX}[1]{\textsf{\STYLE{Key}{`}\texttt{#1}\STYLE{Key}{'}}}
% The following commands produce ASCII characters that are treated specially by LaTeX:
\newcommand{\HASH}{\char`\#}
\newcommand{\DOLLAR}{\char`\$}
\newcommand{\PERCENT}{\char`\%}
\newcommand{\AMPERSAND}{\char`\&}
\newcommand{\APOSTROPHE}{\char`\'}
\newcommand{\BACKSLASH}{\char`\\}
\newcommand{\CARET}{\char`\^}
\newcommand{\UNDERSCORE}{\char`\_}
\newcommand{\GRAVE}{\char`\`}
\newcommand{\LEFTBRACE}{\char`\{}
\newcommand{\RIGHTBRACE}{\char`\}}
\newcommand{\TILDE}{\textasciitilde} % {\char`\~}
% \NAME{name} highlights the name;
% \NAMEDECL{name} declares Name.name as the target of links to name;
% \NAMEREF{name} links name to the target Name.name in the current file;
% \NAMEHYPER{url}{file}{name} links name to Name.name at url/file/file.pdf.
% Similarly for \VAR{partvariable}, \SYN{syntaxname}, \SEM{semanticsName},
% and \SECT{sectionnumber}
% The kerns in \SUB and \VAR avoid overlaps with primes:
\newcommand{\SUB}[1]{_{\kern-2mu\STYLE{PartVariable}{\textsf{#1}}}}
% PLAIN
\newcommand{\VAR}[1]{\STYLE{PartVariable}{\textsf{\textit{#1}\kern2mu}}}
\newcommand{\NAME}[1]{\STYLE{Name}{\textsf{#1}}}
\newcommand{\SYN}[1]{\STYLE{SyntaxName}{\textsf{#1}}}
\newcommand{\SEM}[1]{\STYLE{SemanticsName}{\textsf{#1}}}
\newcommand{\SECT}[1]{\STYLE{SectionNumber}{\textsf{#1}}}
% DECL
\newcommand{\VARDECL}[1]{\DECL{PartVariable}{#1}{\VAR{#1}}}
\newcommand{\NAMEDECL}[1]{\DECL{Name}{#1}{\NAME{#1}}}
\newcommand{\SYNDECL}[1]{\DECL{SyntaxName}{#1}{\SYN{#1}}}
\newcommand{\SEMDECL}[1]{\DECL{SemanticsName}{#1}{\SEM{#1}}}
\newcommand{\SECTDECL}[1]{\DECL{SectionNumber}{#1}{\textsf{#1}}}
% REF
\newcommand{\VARREF}[1]{\REF{PartVariable}{#1}{\VAR{#1}}}
\newcommand{\NAMEREF}[1]{\REF{Name}{#1}{\NAME{#1}}}
\newcommand{\SYNREF}[1]{\REF{SyntaxName}{#1}{\SYN{#1}}}
\newcommand{\SEMREF}[1]{\REF{SemanticsName}{#1}{\SEM{#1}}}
\newcommand{\SECTREF}[1]{\REF{SectionNumber}{#1}{\SECT{#1}}}
% HYPER
\newcommand{\VARHYPER}[3]{\HYPER{#1}{#2}{PartVariable}{#3}{\VAR{#3}}}
\newcommand{\NAMEHYPER}[3]{\HYPER{#1}{#2}{Name}{#3}{\NAME{#3}}}
\newcommand{\SYNHYPER}[3]{\HYPER{#1}{#2}{SyntaxName}{#3}{\SYN{#3}}}
\newcommand{\SEMHYPER}[3]{\HYPER{#1}{#2}{SemanticsName}{#3}{\SEM{#3}}}
\newcommand{\SECTHYPER}[3]{\HYPER{#1}{#2}{SectionNumber}{#3}{\SECT{#3}}}
% \LEFTPHRASE MATH \RIGHTPHRASE produces [[ MATH ]] with proper brackets:
\newcommand{\LEFTPHRASE}{\llbracket}
\newcommand{\RIGHTPHRASE}{\rrbracket}
% \LEFTGROUP MATH \RIGHTGROUP produces ( MATH ) where the parentheses are
% highlighted the same as keywords:
\newcommand{\LEFTGROUP}{\STYLE{Key}{(}}
\newcommand{\RIGHTGROUP}{\STYLE{Key}{)}}
% MATH\PLUS produces a superscript +
% MATH\STAR produces a superscript *
% MATH\QUERY produces a superscript ?
\newcommand{\PLUS}{{}^{\texttt{+}}}
\newcommand{\STAR}{{}^{\texttt{*}}}
\newcommand{\QUERY}{{}^{\texttt{?}}}
% \RULE{& PREMISE \\ & ...}{& FORMULA ... \\ & ...} produces an inference rule
% with separately aligned premises and conclusion
% PREMISE
% ...
% -----------
% FORMULA ...
% ...
\newcommand{\RULE}[2]
{\frac{\begin{aligned}#1\end{aligned}}{\begin{aligned}#2\end{aligned}}}
% \AXIOM{& FORMULA ... \\ & ...} produces an aligned formula
%
% FORMULA ...
% ...
\newcommand{\AXIOM}[1]{\begin{aligned}#1\end{aligned}}
% \TO TYPE produces => TYPE
\newcommand{\TO}{\mathop{\Rightarrow}}
% TERM \TRANS TERM produces TERM ---> TERM
\newcommand{\TRANS}{\longrightarrow}
% TERM \xrightarrow{LABEL} TERM puts the label above the long arrow
%
\)
Sequences of two or more values are not themselves values, nor is the empty
sequence a value. However, sequences can be provided to funcons as arguments,
and returned as results. Many operations on composite values can be expressed
by extracting their components as sequences, operating on the sequences, then
forming the required composite values from the resulting sequences.
A sequence with elements \(\SHADE{\VAR{X}\SUB{1}}\), …, \(\SHADE{\VAR{X}\SUB{n}}\) is written \(\SHADE{\VAR{X}\SUB{1}, \cdots, \VAR{X}\SUB{n}}\).
A sequence with a single element \(\SHADE{\VAR{X}}\) is identified with (and written) \(\SHADE{\VAR{X}}\).
An empty sequence is indicated by the absence of a term.
Any sequence \(\SHADE{\VAR{X}\STAR}\) can be enclosed in parentheses \(\SHADE{( \VAR{X}\STAR )}\), e.g.:
\(\SHADE{( \ )}\), \(\SHADE{( 1 )}\), \(\SHADE{( 1,
2,
3 )}\). Superfluous commas are ignored.
The elements of a type sequence \(\SHADE{\VAR{T}\SUB{1}, \cdots, \VAR{T}\SUB{n}}\) are the value sequences \(\SHADE{\VAR{V}\SUB{1}, \cdots, \VAR{V}\SUB{n}}\)
where \(\SHADE{\VAR{V}\SUB{1} : \VAR{T}\SUB{1}}\), …, \(\SHADE{\VAR{V}\SUB{n} : \VAR{T}\SUB{n}}\). The only element of the empty type sequence \(\SHADE{( \ )}\)
is the empty value sequence \(\SHADE{( \ )}\).
\(\SHADE{( \VAR{T} )^{\VAR{N}}}\) is equivalent to \(\SHADE{\VAR{T}, \cdots, \VAR{T}}\) with \(\SHADE{\VAR{N}}\) occurrences of \(\SHADE{\VAR{T}}\).
\(\SHADE{( \VAR{T} )\STAR}\) is equivalent to the union of all \(\SHADE{( \VAR{T} )^{\VAR{N}}}\) for \(\SHADE{\VAR{N}}\)>=0,
\(\SHADE{( \VAR{T} )\PLUS}\) is equivalent to the union of all \(\SHADE{( \VAR{T} )^{\VAR{N}}}\) for \(\SHADE{\VAR{N}}\)>=1, and
\(\SHADE{( \VAR{T} )\QUERY}\) is equivalent to \(\SHADE{\VAR{T} \mid ( \ )}\).
The parentheses around \(\SHADE{\VAR{T}}\) above can be omitted when they are not needed for
disambiguation.
(Non-trivial) sequence types are not values, so not included in \(\SHADE{\NAMEHYPER{../..}{Value-Types}{types}}\).
\(\SHADE{\NAMEREF{index}
( \VAR{N},
\VAR{V}\STAR )}\) gives the \(\SHADE{\VAR{N}}\)th element of \(\SHADE{\VAR{V}\STAR}\), if it exists, otherwise \(\SHADE{( \ )}\).