Values
The grammar productions in this section define lexical syntax,
hence no white space is allowed.
Integers
All integers can be written in either decimal or hexadecimal notation.
In both cases, digits can optionally be separated by underscores.
\[\begin{split}\begin{array}{llclll@{\qquad}l}
\def\mathdef4343#1{{}}\mathdef4343{sign} & \href{../text/values.html#text-sign}{\mathtt{sign}} &::=&
\epsilon \Rightarrow {+} ~~|~~
\def\mathdef4382#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4382{+} \Rightarrow {+} ~~|~~
\def\mathdef4383#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4383{-} \Rightarrow {-} \\
\def\mathdef4343#1{{}}\mathdef4343{decimal digit} & \href{../text/values.html#text-digit}{\mathtt{digit}} &::=&
\def\mathdef4384#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4384{0} \Rightarrow 0 ~~|~~ \dots ~~|~~ \def\mathdef4385#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4385{9} \Rightarrow 9 \\
\def\mathdef4343#1{{}}\mathdef4343{hexadecimal digit} & \href{../text/values.html#text-hexdigit}{\mathtt{hexdigit}} &::=&
d{:}\href{../text/values.html#text-digit}{\mathtt{digit}} \Rightarrow d \\ &&|&
\def\mathdef4386#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4386{A} \Rightarrow 10 ~~|~~ \dots ~~|~~ \def\mathdef4387#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4387{F} \Rightarrow 15 \\ &&|&
\def\mathdef4388#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4388{a} \Rightarrow 10 ~~|~~ \dots ~~|~~ \def\mathdef4389#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4389{f} \Rightarrow 15
\\[1ex]
\def\mathdef4343#1{{}}\mathdef4343{decimal number} & \href{../text/values.html#text-num}{\mathtt{num}} &::=&
d{:}\href{../text/values.html#text-digit}{\mathtt{digit}} &\Rightarrow& d \\ &&|&
n{:}\href{../text/values.html#text-num}{\mathtt{num}}~~\def\mathdef4390#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4390{\_}^?~~d{:}\href{../text/values.html#text-digit}{\mathtt{digit}} &\Rightarrow& 10\cdot n + d \\
\def\mathdef4343#1{{}}\mathdef4343{hexadecimal number} & \href{../text/values.html#text-hexnum}{\mathtt{hexnum}} &::=&
h{:}\href{../text/values.html#text-hexdigit}{\mathtt{hexdigit}} &\Rightarrow& h \\ &&|&
n{:}\href{../text/values.html#text-hexnum}{\mathtt{hexnum}}~~\def\mathdef4391#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4391{\_}^?~~h{:}\href{../text/values.html#text-hexdigit}{\mathtt{hexdigit}} &\Rightarrow& 16\cdot n + h \\
\end{array}\end{split}\]
The allowed syntax for integer literals depends on size and signedness.
Moreover, their value must lie within the range of the respective type.
\[\begin{split}\begin{array}{llclll@{\qquad}l}
\def\mathdef4343#1{{}}\mathdef4343{unsigned integer} & \href{../text/values.html#text-int}{\def\mathdef4364#1{{\mathtt{u}#1}}\mathdef4364{N}} &::=&
n{:}\href{../text/values.html#text-num}{\mathtt{num}} &\Rightarrow& n & (\mathrel{\mbox{if}} n < 2^N) \\ &&|&
\def\mathdef4392#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4392{0x}~~n{:}\href{../text/values.html#text-hexnum}{\mathtt{hexnum}} &\Rightarrow& n & (\mathrel{\mbox{if}} n < 2^N) \\
\def\mathdef4343#1{{}}\mathdef4343{signed integer} & \href{../text/values.html#text-int}{\def\mathdef4370#1{{\mathtt{s}#1}}\mathdef4370{N}} &::=&
{\pm}{:}\href{../text/values.html#text-sign}{\mathtt{sign}}~~n{:}\href{../text/values.html#text-num}{\mathtt{num}} &\Rightarrow& \pm n & (\mathrel{\mbox{if}} -2^{N-1} \leq \pm n < 2^{N-1}) \\ &&|&
{\pm}{:}\href{../text/values.html#text-sign}{\mathtt{sign}}~~\def\mathdef4393#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4393{0x}~~n{:}\href{../text/values.html#text-hexnum}{\mathtt{hexnum}} &\Rightarrow& \pm n & (\mathrel{\mbox{if}} -2^{N-1} \leq \pm n < 2^{N-1}) \\
\end{array}\end{split}\]
Uninterpreted integers can be written as either signed or unsigned, and are normalized to unsigned in the abstract syntax.
\[\begin{split}\begin{array}{llclll@{\qquad\qquad}l}
\def\mathdef4343#1{{}}\mathdef4343{uninterpreted integers} & \href{../text/values.html#text-int}{\def\mathdef4373#1{{\mathtt{i}#1}}\mathdef4373{N}} &::=&
n{:}\href{../text/values.html#text-int}{\def\mathdef4364#1{{\mathtt{u}#1}}\mathdef4364{N}} &\Rightarrow& n \\ &&|&
i{:}\href{../text/values.html#text-int}{\def\mathdef4370#1{{\mathtt{s}#1}}\mathdef4370{N}} &\Rightarrow& n & (\mathrel{\mbox{if}} i = \href{../exec/numerics.html#aux-signed}{\mathrm{signed}}(n)) \\
\end{array}\end{split}\]
Floating-Point
Floating-point values can be represented in either decimal or hexadecimal notation.
\[\begin{split}\begin{array}{llclll@{\qquad\qquad}l}
\def\mathdef4343#1{{}}\mathdef4343{decimal floating-point fraction} & \href{../text/values.html#text-frac}{\mathtt{frac}} &::=&
d{:}\href{../text/values.html#text-digit}{\mathtt{digit}} &\Rightarrow& d/10 \\ &&|&
d{:}\href{../text/values.html#text-digit}{\mathtt{digit}}~~\def\mathdef4394#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4394{\_}^?~~p{:}\href{../text/values.html#text-frac}{\mathtt{frac}} &\Rightarrow& (d+p/10)/10 \\
\def\mathdef4343#1{{}}\mathdef4343{hexadecimal floating-point fraction} & \href{../text/values.html#text-hexfrac}{\mathtt{hexfrac}} &::=&
h{:}\href{../text/values.html#text-hexdigit}{\mathtt{hexdigit}} &\Rightarrow& h/16 \\ &&|&
h{:}\href{../text/values.html#text-hexdigit}{\mathtt{hexdigit}}~~\def\mathdef4395#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4395{\_}^?~~p{:}\href{../text/values.html#text-hexfrac}{\mathtt{hexfrac}} &\Rightarrow& (h+p/16)/16 \\
\def\mathdef4343#1{{}}\mathdef4343{decimal floating-point number} & \href{../text/values.html#text-float}{\mathtt{float}} &::=&
p{:}\href{../text/values.html#text-num}{\mathtt{num}}~\def\mathdef4396#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4396{.}^?
&\Rightarrow& p \\ &&|&
p{:}\href{../text/values.html#text-num}{\mathtt{num}}~\def\mathdef4397#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4397{.}~q{:}\href{../text/values.html#text-frac}{\mathtt{frac}}
&\Rightarrow& p+q \\ &&|&
p{:}\href{../text/values.html#text-num}{\mathtt{num}}~\def\mathdef4398#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4398{.}^?~(\def\mathdef4399#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4399{E}~|~\def\mathdef4400#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4400{e})~{\pm}{:}\href{../text/values.html#text-sign}{\mathtt{sign}}~e{:}\href{../text/values.html#text-num}{\mathtt{num}}
&\Rightarrow& p\cdot 10^{\pm e} \\ &&|&
p{:}\href{../text/values.html#text-num}{\mathtt{num}}~\def\mathdef4401#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4401{.}~q{:}\href{../text/values.html#text-frac}{\mathtt{frac}}~(\def\mathdef4402#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4402{E}~|~\def\mathdef4403#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4403{e})~{\pm}{:}\href{../text/values.html#text-sign}{\mathtt{sign}}~e{:}\href{../text/values.html#text-num}{\mathtt{num}}
&\Rightarrow& (p+q)\cdot 10^{\pm e} \\
\def\mathdef4343#1{{}}\mathdef4343{hexadecimal floating-point number} & \href{../text/values.html#text-hexfloat}{\mathtt{hexfloat}} &::=&
\def\mathdef4404#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4404{0x}~p{:}\href{../text/values.html#text-hexnum}{\mathtt{hexnum}}~\def\mathdef4405#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4405{.}^?
&\Rightarrow& p \\ &&|&
\def\mathdef4406#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4406{0x}~p{:}\href{../text/values.html#text-hexnum}{\mathtt{hexnum}}~\def\mathdef4407#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4407{.}~q{:}\href{../text/values.html#text-hexfrac}{\mathtt{hexfrac}}
&\Rightarrow& p+q \\ &&|&
\def\mathdef4408#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4408{0x}~p{:}\href{../text/values.html#text-hexnum}{\mathtt{hexnum}}~\def\mathdef4409#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4409{.}^?~(\def\mathdef4410#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4410{P}~|~\def\mathdef4411#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4411{p})~{\pm}{:}\href{../text/values.html#text-sign}{\mathtt{sign}}~e{:}\href{../text/values.html#text-num}{\mathtt{num}}
&\Rightarrow& p\cdot 2^{\pm e} \\ &&|&
\def\mathdef4412#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4412{0x}~p{:}\href{../text/values.html#text-hexnum}{\mathtt{hexnum}}~\def\mathdef4413#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4413{.}~q{:}\href{../text/values.html#text-hexfrac}{\mathtt{hexfrac}}~(\def\mathdef4414#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4414{P}~|~\def\mathdef4415#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4415{p})~{\pm}{:}\href{../text/values.html#text-sign}{\mathtt{sign}}~e{:}\href{../text/values.html#text-num}{\mathtt{num}}
&\Rightarrow& (p+q)\cdot 2^{\pm e}
\end{array}\end{split}\]
The value of a literal must not lie outside the representable range of the corresponding IEEE 754 type
(that is, a numeric value must not overflow to \(\pm\mbox{infinity}\)),
but it may be rounded to the nearest representable value.
Note
Rounding can be prevented by using hexadecimal notation with no more significant bits than supported by the required type.
Floating-point values may also be written as constants for infinity or canonical NaN (not a number).
Furthermore, arbitrary NaN values may be expressed by providing an explicit payload value.
\[\begin{split}\begin{array}{llclll@{\qquad\qquad}l}
\def\mathdef4343#1{{}}\mathdef4343{floating-point value} & \href{../text/values.html#text-float}{\def\mathdef4378#1{{\mathtt{f}#1}}\mathdef4378{N}} &::=&
{\pm}{:}\href{../text/values.html#text-sign}{\mathtt{sign}}~z{:}\href{../text/values.html#text-float}{\def\mathdef4379#1{{\mathtt{f}#1}}\mathdef4379{N}\mathtt{mag}} &\Rightarrow& \pm z \\
\def\mathdef4343#1{{}}\mathdef4343{floating-point magnitude} & \href{../text/values.html#text-float}{\def\mathdef4379#1{{\mathtt{f}#1}}\mathdef4379{N}\mathtt{mag}} &::=&
z{:}\href{../text/values.html#text-float}{\mathtt{float}} &\Rightarrow& \href{../exec/numerics.html#aux-ieee}{\mathrm{float}}_N(z) & (\mathrel{\mbox{if}} \href{../exec/numerics.html#aux-ieee}{\mathrm{float}}_N(z) \neq \pm \infty) \\ &&|&
z{:}\href{../text/values.html#text-hexfloat}{\mathtt{hexfloat}} &\Rightarrow& \href{../exec/numerics.html#aux-ieee}{\mathrm{float}}_N(z) & (\mathrel{\mbox{if}} \href{../exec/numerics.html#aux-ieee}{\mathrm{float}}_N(z) \neq \pm \infty) \\ &&|&
\def\mathdef4416#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4416{inf} &\Rightarrow& \infty \\ &&|&
\def\mathdef4417#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4417{nan} &\Rightarrow& \href{../syntax/values.html#syntax-float}{\mathsf{nan}}(\href{../syntax/values.html#aux-canon}{\mathrm{canon}}_N) \\ &&|&
\def\mathdef4418#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4418{nan{:}0x}~n{:}\href{../text/values.html#text-hexnum}{\mathtt{hexnum}} &\Rightarrow& \href{../syntax/values.html#syntax-float}{\mathsf{nan}}(n) & (\mathrel{\mbox{if}} 1 \leq n < 2^{\href{../syntax/values.html#aux-significand}{\mathrm{signif}}(N)}) \\
\end{array}\end{split}\]
Strings
Strings denote sequences of bytes that can represent both textual and binary data.
They are enclosed in quotation marks
and may contain any character other than ASCII control characters, quotation marks (\(\def\mathdef4419#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4419{"}\)), or backslash (\(\def\mathdef4420#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4420{\backslash}\)),
except when expressed with an escape sequence.
\[\begin{split}\begin{array}{llclll@{\qquad\qquad}l}
\def\mathdef4343#1{{}}\mathdef4343{string} & \href{../text/values.html#text-string}{\mathtt{string}} &::=&
\def\mathdef4421#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4421{"}~(b^\ast{:}\href{../text/values.html#text-string}{\mathtt{stringelem}})^\ast~\def\mathdef4422#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4422{"}
&\Rightarrow& \href{../syntax/conventions.html#notation-concat}{\mathrm{concat}}((b^\ast)^\ast)
& (\mathrel{\mbox{if}} |\href{../syntax/conventions.html#notation-concat}{\mathrm{concat}}((b^\ast)^\ast)| < 2^{32}) \\
\def\mathdef4343#1{{}}\mathdef4343{string element} & \href{../text/values.html#text-string}{\mathtt{stringelem}} &::=&
c{:}\href{../text/values.html#text-string}{\mathtt{stringchar}} &\Rightarrow& \href{../binary/values.html#binary-utf8}{\mathrm{utf8}}(c) \\ &&|&
\def\mathdef4423#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4423{\backslash}~n{:}\href{../text/values.html#text-hexdigit}{\mathtt{hexdigit}}~m{:}\href{../text/values.html#text-hexdigit}{\mathtt{hexdigit}}
&\Rightarrow& 16\cdot n+m \\
\end{array}\end{split}\]
Each character in a string literal represents the byte sequence corresponding to its UTF-8 Unicode (Section 2.5) encoding,
except for hexadecimal escape sequences \(\mbox{‘}\backslash hh\mbox{’}\), which represent raw bytes of the respective value.
\[\begin{split}\begin{array}{llclll@{\qquad\qquad}l}
\def\mathdef4343#1{{}}\mathdef4343{string character} & \href{../text/values.html#text-string}{\mathtt{stringchar}} &::=&
c{:}\href{../text/lexical.html#text-char}{\mathtt{char}} &\Rightarrow& c \qquad
& (\mathrel{\mbox{if}} c \geq \def\mathdef4424#1{\mathrm{U{+}#1}}\mathdef4424{20} \wedge c \neq \def\mathdef4425#1{\mathrm{U{+}#1}}\mathdef4425{7F} \wedge c \neq \def\mathdef4426#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4426{"} \wedge c \neq \def\mathdef4427#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4427{\backslash}) \\ &&|&
\def\mathdef4428#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4428{\backslash t} &\Rightarrow& \def\mathdef4429#1{\mathrm{U{+}#1}}\mathdef4429{09} \\ &&|&
\def\mathdef4430#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4430{\backslash n} &\Rightarrow& \def\mathdef4431#1{\mathrm{U{+}#1}}\mathdef4431{0A} \\ &&|&
\def\mathdef4432#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4432{\backslash r} &\Rightarrow& \def\mathdef4433#1{\mathrm{U{+}#1}}\mathdef4433{0D} \\ &&|&
\def\mathdef4434#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4434{\backslash{"}} &\Rightarrow& \def\mathdef4435#1{\mathrm{U{+}#1}}\mathdef4435{22} \\ &&|&
\def\mathdef4436#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4436{\backslash{'}} &\Rightarrow& \def\mathdef4437#1{\mathrm{U{+}#1}}\mathdef4437{27} \\ &&|&
\def\mathdef4438#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4438{\backslash\backslash} &\Rightarrow& \def\mathdef4439#1{\mathrm{U{+}#1}}\mathdef4439{5C} \\ &&|&
\def\mathdef4440#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4440{\backslash u\{}~n{:}\href{../text/values.html#text-hexnum}{\mathtt{hexnum}}~\def\mathdef4441#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4441{\}}
&\Rightarrow& \def\mathdef4442#1{\mathrm{U{+}#1}}\mathdef4442{(n)} & (\mathrel{\mbox{if}} n < \def\mathdef4443#1{\mathtt{0x#1}}\mathdef4443{D800} \vee \def\mathdef4444#1{\mathtt{0x#1}}\mathdef4444{E000} \leq n < \def\mathdef4445#1{\mathtt{0x#1}}\mathdef4445{110000}) \\
\end{array}\end{split}\]
Names
Names are strings denoting a literal character sequence.
A name string must form a valid UTF-8 encoding as defined by Unicode (Section 2.5) and is interpreted as a string of Unicode scalar values.
\[\begin{split}\begin{array}{llclll@{\qquad}l}
\def\mathdef4343#1{{}}\mathdef4343{name} & \href{../text/values.html#text-name}{\mathtt{name}} &::=&
b^\ast{:}\href{../text/values.html#text-string}{\mathtt{string}} &\Rightarrow& c^\ast & (\mathrel{\mbox{if}} b^\ast = \href{../binary/values.html#binary-utf8}{\mathrm{utf8}}(c^\ast)) \\
\end{array}\end{split}\]
Note
Presuming the source text is itself encoded correctly,
strings that do not contain any uses of hexadecimal byte escapes are always valid names.
Identifiers
Indices can be given in both numeric and symbolic form.
Symbolic identifiers that stand in lieu of indices start with \(\def\mathdef4446#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4446{\$}\), followed by any sequence of printable ASCII characters that does not contain a space, quotation mark, comma, semicolon, or bracket.
\[\begin{split}\begin{array}{llclll@{\qquad}l}
\def\mathdef4343#1{{}}\mathdef4343{identifier} & \href{../text/values.html#text-id}{\mathtt{id}} &::=&
\def\mathdef4447#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4447{\$}~\href{../text/values.html#text-idchar}{\mathtt{idchar}}^+ \\
\def\mathdef4343#1{{}}\mathdef4343{identifier character} & \href{../text/values.html#text-idchar}{\mathtt{idchar}} &::=&
\def\mathdef4448#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4448{0} ~~|~~ \dots ~~|~~ \def\mathdef4449#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4449{9} \\ &&|&
\def\mathdef4450#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4450{A} ~~|~~ \dots ~~|~~ \def\mathdef4451#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4451{Z} \\ &&|&
\def\mathdef4452#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4452{a} ~~|~~ \dots ~~|~~ \def\mathdef4453#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4453{z} \\ &&|&
\def\mathdef4454#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4454{!} ~~|~~
\def\mathdef4455#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4455{\#} ~~|~~
\def\mathdef4456#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4456{\$} ~~|~~
\def\mathdef4457#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4457{\%} ~~|~~
\def\mathdef4458#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4458{\&} ~~|~~
\def\mathdef4459#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4459{'} ~~|~~
\def\mathdef4460#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4460{*} ~~|~~
\def\mathdef4461#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4461{+} ~~|~~
\def\mathdef4462#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4462{-} ~~|~~
\def\mathdef4463#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4463{.} ~~|~~
\def\mathdef4464#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4464{/} \\ &&|&
\def\mathdef4465#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4465{:} ~~|~~
\def\mathdef4466#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4466{<} ~~|~~
\def\mathdef4467#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4467{=} ~~|~~
\def\mathdef4468#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4468{>} ~~|~~
\def\mathdef4469#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4469{?} ~~|~~
\def\mathdef4470#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4470{@} ~~|~~
\def\mathdef4471#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4471{\backslash} ~~|~~
\def\mathdef4472#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4472{\hat{~~}} ~~|~~
\def\mathdef4473#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4473{\_} ~~|~~
\def\mathdef4474#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4474{\grave{~~}} ~~|~~
\def\mathdef4475#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4475{|} ~~|~~
\def\mathdef4476#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4476{\tilde{~~}} \\
\end{array}\end{split}\]
Conventions
The expansion rules of some abbreviations require insertion of a fresh identifier.
That may be any syntactically valid identifier that does not already occur in the given source text.