macros.def

.. LINK MACROS

.. External Standards
.. ------------------

.. |WasmDraft| replace:: |pagelink|
.. _WasmDraft: |pagelink|

.. |WasmIssues| replace:: |issuelink|
.. _WasmIssues: |issuelink|

.. |IEEE754| replace:: IEEE 754
.. _IEEE754: https://ieeexplore.ieee.org/document/8766229

.. |Unicode| replace:: Unicode
.. _Unicode: https://www.unicode.org/versions/latest/

.. |ASCII| replace:: ASCII
.. _ASCII: https://webstore.ansi.org/RecordDetail.aspx?sku=INCITS+4-1986%5bR2012%5d


.. External Definitions
.. --------------------

.. |LittleEndian| replace:: little endian
.. _LittleEndian: https://en.wikipedia.org/wiki/Endianness#Little-endian

.. |LEB128| replace:: LEB128
.. _LEB128: https://en.wikipedia.org/wiki/LEB128
.. |UnsignedLEB128| replace:: unsigned LEB128
.. _UnsignedLEB128: https://en.wikipedia.org/wiki/LEB128#Unsigned_LEB128
.. |SignedLEB128| replace:: signed LEB128
.. _SignedLEB128: https://en.wikipedia.org/wiki/LEB128#Signed_LEB128

.. |SExpressions| replace:: S-expressions
.. _SExpressions: https://en.wikipedia.org/wiki/S-expression

.. |MediaType| replace:: Media Type
.. _MediaType: https://www.iana.org/assignments/media-types/media-types.xhtml


.. Literature
.. ----------

.. |PLDI2017| replace:: Bringing the Web up to Speed with WebAssembly
.. _PLDI2017: https://dl.acm.org/citation.cfm?doid=3062341.3062363

.. |CPP2018| replace:: Mechanising and Verifying the WebAssembly Specification
.. _CPP2018: https://dl.acm.org/citation.cfm?id=3167082

.. |FM2021| replace:: Two Mechanisations of WebAssembly 1.0
.. _FM2021: https://link.springer.com/chapter/10.1007/978-3-030-90870-6_4

.. |TAPL| replace:: Types and Programming Languages
.. _TAPL: https://www.cis.upenn.edu/~bcpierce/tapl/



.. MATH MACROS


.. Generic Stuff
.. -------------

.. To comment out stuff

.. |void#1| mathdef:: {}


.. Type-setting of names
.. X - (multi-letter) variables / non-terminals
.. F - functions
.. K - keywords / terminals
.. B - binary grammar non-terminals
.. T - textual grammar non-terminals

.. |X| mathdef:: \mathit
.. |F| mathdef:: \mathrm
.. |K| mathdef:: \mathsf
.. |B| mathdef:: \mathtt
.. |T| mathdef:: \mathtt


.. Notation

.. |mod| mathdef:: \mathbin{\F{mod}}

.. |iff| mathdef:: \mathrel{\mbox{if}}
.. |otherwise| mathdef:: \mathrel{\mbox{otherwise}}
.. |where| mathdef:: \mathrel{\mbox{where}}



.. Grammar & Syntax Notation
.. -------------------------

.. Notation for grammars

.. |production| mathdef:: \void


.. Notation for Sequences & Records

.. |subst| mathdef:: \xref{valid/conventions}{notation-subst}{\mathrel{\mathbf{:=}}}
.. |slice| mathdef:: \xref{syntax/conventions}{notation-slice}{\mathrel{\mathbf{:}}}
.. |with| mathdef:: \xref{syntax/conventions}{notation-replace}{\mathrel{\mbox{with}}}
.. |cat| mathdef:: \xref{syntax/conventions}{notation-concat}{\oplus}
.. |bigcat| mathdef:: \xref{syntax/conventions}{notation-concat}{\bigoplus}
.. |concat| mathdef:: \xref{syntax/conventions}{notation-concat}{\bigoplus}
.. |compose| mathdef:: \xref{syntax/conventions}{notation-compose}{\oplus}
.. |bigcompose| mathdef:: \xref{syntax/conventions}{notation-compose}{\bigoplus}


.. Profile Annotations
.. -------------------

.. |exprofiles#1| mathdef:: {{}^{\small{[{!}#1]}}}
.. |profilename#1| mathdef:: {\small{\mathrm{#1}}}
.. |profile| mathdef:: \mathrm

.. |PROFFULL| mathdef:: \xref{appendix/profiles}{profile-full}{\profile{FUL}}
.. |PROFDET| mathdef:: \xref{appendix/profiles}{profile-deterministic}{\profile{DET}}
.. |EXPROFDET| mathdef:: \exprofiles{\PROFDET}



.. Abstract Syntax
.. ---------------

.. Auxiliary productions

.. |list| mathdef:: \xref{syntax/conventions}{syntax-list}{\X{list}}


.. Values, terminals

.. |hex#1| mathdef:: \mathtt{0x#1}
.. |unicode#1| mathdef:: \mathrm{U{+}#1}

.. |NAN| mathdef:: \xref{syntax/values}{syntax-float}{\K{nan}}


.. Values, non-terminals

.. |byte| mathdef:: \xref{syntax/values}{syntax-byte}{\X{byte}}

.. |uX#1| mathdef:: {\X{u#1}}
.. |sX#1| mathdef:: {\X{s#1}}
.. |iX#1| mathdef:: {\X{i#1}}
.. |fX#1| mathdef:: {\X{f#1}}
.. |vX#1| mathdef:: {\X{v#1}}

.. |uNX| mathdef:: \xref{syntax/values}{syntax-int}{\X{u}\kern-0.1em}
.. |uN| mathdef:: \xref{syntax/values}{syntax-int}{\X{u}\scriptstyle\kern-0.1emN}
.. |u1| mathdef:: \xref{syntax/values}{syntax-int}{\X{u\scriptstyle\kern-0.1em1}}
.. |u8| mathdef:: \xref{syntax/values}{syntax-int}{\X{u\scriptstyle\kern-0.1em8}}
.. |u16| mathdef:: \xref{syntax/values}{syntax-int}{\X{u\scriptstyle\kern-0.1em16}}
.. |u31| mathdef:: \xref{syntax/values}{syntax-int}{\X{u\scriptstyle\kern-0.1em31}}
.. |u32| mathdef:: \xref{syntax/values}{syntax-int}{\X{u\scriptstyle\kern-0.1em32}}
.. |u64| mathdef:: \xref{syntax/values}{syntax-int}{\X{u\scriptstyle\kern-0.1em64}}
.. |u128| mathdef:: \xref{syntax/values}{syntax-int}{\X{u\scriptstyle\kern-0.1em128}}

.. |sNX| mathdef:: \xref{syntax/values}{syntax-int}{\X{s}\kern-0.1em}
.. |sN| mathdef:: \xref{syntax/values}{syntax-int}{\X{s}\scriptstyle\kern-0.1emN}
.. |s8| mathdef:: \xref{syntax/values}{syntax-int}{\X{s\scriptstyle\kern-0.1em8}}
.. |s16| mathdef:: \xref{syntax/values}{syntax-int}{\X{s\scriptstyle\kern-0.1em16}}
.. |s32| mathdef:: \xref{syntax/values}{syntax-int}{\X{s\scriptstyle\kern-0.1em32}}
.. |s64| mathdef:: \xref{syntax/values}{syntax-int}{\X{s\scriptstyle\kern-0.1em64}}

.. |iNX| mathdef:: \xref{syntax/values}{syntax-int}{\X{i}\kern-0.1em}
.. |iM| mathdef:: \xref{syntax/values}{syntax-int}{\X{i}\scriptstyle\kern-0.1emM}
.. |iN| mathdef:: \xref{syntax/values}{syntax-int}{\X{i}\scriptstyle\kern-0.1emN}
.. |i8| mathdef:: \xref{syntax/values}{syntax-int}{\X{i\scriptstyle\kern-0.1em8}}
.. |i16| mathdef:: \xref{syntax/values}{syntax-int}{\X{i\scriptstyle\kern-0.1em16}}
.. |i32| mathdef:: \xref{syntax/values}{syntax-int}{\X{i\scriptstyle\kern-0.1em32}}
.. |i64| mathdef:: \xref{syntax/values}{syntax-int}{\X{i\scriptstyle\kern-0.1em64}}
.. |i128| mathdef:: \xref{syntax/values}{syntax-int}{\X{i\scriptstyle\kern-0.1em128}}

.. |fNX| mathdef:: \xref{syntax/values}{syntax-float}{\X{f}\kern-0.15em}
.. |fN| mathdef:: \xref{syntax/values}{syntax-float}{\X{f}\scriptstyle\kern-0.15emN}
.. |fNmag| mathdef:: \xref{syntax/values}{syntax-float}{\X{fmag}\scriptstyle\kern-0.1emN}
.. |f32| mathdef:: \xref{syntax/values}{syntax-float}{\X{f\scriptstyle\kern-0.15em32}}
.. |f64| mathdef:: \xref{syntax/values}{syntax-float}{\X{f\scriptstyle\kern-0.15em64}}

.. |vNX| mathdef:: \xref{syntax/values}{syntax-vecnum}{\X{v}\kern-0.1em}

.. |name| mathdef:: \xref{syntax/values}{syntax-name}{\X{name}}
.. |char| mathdef:: \xref{syntax/values}{syntax-name}{\X{char}}


.. Values, meta functions

.. |canon| mathdef:: \xref{syntax/values}{aux-canon}{\F{canon}}
.. |signif| mathdef:: \xref{syntax/values}{aux-signif}{\F{signif}}
.. |expon| mathdef:: \xref{syntax/values}{aux-expon}{\F{expon}}


.. Types, terminals

.. |to| mathdef:: \mathrel{\xref{valid/conventions}{syntax-instrtype}{\rightarrow}}
.. |toM| mathdef:: \mathrel{\xref{valid/modules}{syntax-moduletype}{\rightarrow}}

.. |BOTH| mathdef:: \xref{valid/conventions}{syntax-heaptype-ext}{\K{bot}}
.. |BOT| mathdef:: \xref{valid/conventions}{syntax-valtype-ext}{\K{bot}}

.. |I8| mathdef:: \xref{syntax/types}{syntax-storagetype}{\K{i\scriptstyle8}}
.. |I16| mathdef:: \xref{syntax/types}{syntax-storagetype}{\K{i\scriptstyle16}}
.. |I32| mathdef:: \xref{syntax/types}{syntax-numtype}{\K{i\scriptstyle32}}
.. |I64| mathdef:: \xref{syntax/types}{syntax-numtype}{\K{i\scriptstyle64}}
.. |F32| mathdef:: \xref{syntax/types}{syntax-numtype}{\K{f\scriptstyle32}}
.. |F64| mathdef:: \xref{syntax/types}{syntax-numtype}{\K{f\scriptstyle64}}
.. |I128| mathdef:: \xref{syntax/types}{syntax-vectype}{\K{i\scriptstyle128}}
.. |V128| mathdef:: \xref{syntax/types}{syntax-vectype}{\K{v\scriptstyle128}}
.. |INX| mathdef:: \xref{syntax/types}{syntax-numtype}{\K{i}}
.. |IN| mathdef:: \xref{syntax/types}{syntax-numtype}{\K{i}\scriptstyle\kern-0.1emN}
.. |FNX| mathdef:: \xref{syntax/types}{syntax-numtype}{\K{f}}
.. |FN| mathdef:: \xref{syntax/types}{syntax-numtype}{\K{f}\scriptstyle\kern-0.1emN}
.. |VNX| mathdef:: \xref{syntax/types}{syntax-vectype}{\K{v}}
.. |VN| mathdef:: \xref{syntax/types}{syntax-vectype}{\K{v}\scriptstyle\kern-0.1emN}

.. |ntI| mathdef:: \xref{syntax/types}{syntax-numtype}{\K{i}}
.. |ntF| mathdef:: \xref{syntax/types}{syntax-numtype}{\K{f}}
.. |ntV| mathdef:: \xref{syntax/types}{syntax-numtype}{\K{v}}
.. |ntN| mathdef:: \xref{syntax/types}{syntax-numtype}{\scriptstyle\kern-0.1emN}

.. |ANYREF| mathdef:: \xref{syntax/types}{syntax-reftype}{\K{anyref}}
.. |EQREF| mathdef:: \xref{syntax/types}{syntax-reftype}{\K{eqref}}
.. |I31REF| mathdef:: \xref{syntax/types}{syntax-reftype}{\K{i{\scriptstyle31}ref}}
.. |STRUCTREF| mathdef:: \xref{syntax/types}{syntax-reftype}{\K{structref}}
.. |ARRAYREF| mathdef:: \xref{syntax/types}{syntax-reftype}{\K{arrayref}}
.. |FUNCREF| mathdef:: \xref{syntax/types}{syntax-reftype}{\K{funcref}}
.. |EXNREF| mathdef:: \xref{syntax/types}{syntax-reftype}{\K{exnref}}
.. |EXTERNREF| mathdef:: \xref{syntax/types}{syntax-reftype}{\K{externref}}
.. |NULLREF| mathdef:: \xref{syntax/types}{syntax-reftype}{\K{nullref}}
.. |NULLFUNCREF| mathdef:: \xref{syntax/types}{syntax-reftype}{\K{nullfuncref}}
.. |NULLEXNREF| mathdef:: \xref{syntax/types}{syntax-reftype}{\K{nullexnref}}
.. |NULLEXTERNREF| mathdef:: \xref{syntax/types}{syntax-reftype}{\K{nullexternref}}
.. |REF| mathdef:: \xref{syntax/types}{syntax-reftype}{\K{ref}}
.. |NULL| mathdef:: \xref{syntax/types}{syntax-reftype}{\K{null}}

.. |ANY| mathdef:: \xref{syntax/types}{syntax-heaptype}{\K{any}}
.. |EQT| mathdef:: \xref{syntax/types}{syntax-heaptype}{\K{eq}}
.. |I31| mathdef:: \xref{syntax/types}{syntax-heaptype}{\K{i\scriptstyle31}}
.. |STRUCT| mathdef:: \xref{syntax/types}{syntax-heaptype}{\K{struct}}
.. |ARRAY| mathdef:: \xref{syntax/types}{syntax-heaptype}{\K{array}}
.. |FUNCT| mathdef:: \xref{syntax/types}{syntax-heaptype}{\K{func}}
.. |EXN| mathdef:: \xref{syntax/types}{syntax-heaptype}{\K{exn}}
.. |EXTERN| mathdef:: \xref{syntax/types}{syntax-heaptype}{\K{extern}}
.. |NONE| mathdef:: \xref{syntax/types}{syntax-heaptype}{\K{none}}
.. |NOFUNC| mathdef:: \xref{syntax/types}{syntax-heaptype}{\K{nofunc}}
.. |NOEXN| mathdef:: \xref{syntax/types}{syntax-heaptype}{\K{noexn}}
.. |NOEXTERN| mathdef:: \xref{syntax/types}{syntax-heaptype}{\K{noextern}}

.. |I8X16| mathdef:: \xref{syntax/instructions}{syntax-shape}{\K{i{\scriptstyle8}x\scriptstyle16}}
.. |I16X8| mathdef:: \xref{syntax/instructions}{syntax-shape}{\K{i{\scriptstyle16}x\scriptstyle8}}
.. |I32X4| mathdef:: \xref{syntax/instructions}{syntax-shape}{\K{i{\scriptstyle32}x\scriptstyle4}}
.. |I64X2| mathdef:: \xref{syntax/instructions}{syntax-shape}{\K{i{\scriptstyle64}x\scriptstyle2}}
.. |F32X4| mathdef:: \xref{syntax/instructions}{syntax-shape}{\K{f{\scriptstyle32}x\scriptstyle4}}
.. |F64X2| mathdef:: \xref{syntax/instructions}{syntax-shape}{\K{f{\scriptstyle64}x\scriptstyle2}}

.. |REC| mathdef:: \xref{syntax/types}{syntax-heaptype}{\K{rec}}

.. |TFUNC| mathdef:: \xref{syntax/types}{syntax-comptype}{\K{func}}
.. |Tarrow| mathdef:: \xref{syntax/types}{syntax-comptype}{\rightarrow}
.. |TSTRUCT| mathdef:: \xref{syntax/types}{syntax-comptype}{\K{struct}}
.. |TARRAY| mathdef:: \xref{syntax/types}{syntax-comptype}{\K{array}}
.. |TSUB| mathdef:: \xref{syntax/types}{syntax-subtype}{\K{sub}}
.. |TREC| mathdef:: \xref{syntax/types}{syntax-rectype}{\K{rec}}
.. |TFINAL| mathdef:: \xref{syntax/types}{syntax-subtype}{\K{final}}

.. |TMUT| mathdef:: \xref{syntax/types}{syntax-mut}{\K{mut}}

.. |SET| mathdef:: \xref{valid/conventions}{syntax-init}{\K{set}}
.. |UNSET| mathdef:: \xref{valid/conventions}{syntax-init}{\K{unset}}

.. |Llbrack| mathdef:: \xref{syntax/types}{syntax-limits}{\[}
.. |Lrbrack| mathdef:: \xref{syntax/types}{syntax-limits}{\]}
.. |Ldotdot| mathdef:: \xref{syntax/types}{syntax-limits}{\,{..}\,}
.. |PAGE| mathdef:: \xref{syntax/types}{syntax-memtype}{\K{page}}

.. |XTFUNC| mathdef:: \xref{syntax/types}{syntax-externtype}{\K{func}}
.. |XTTABLE| mathdef:: \xref{syntax/types}{syntax-externtype}{\K{table}}
.. |XTMEM| mathdef:: \xref{syntax/types}{syntax-externtype}{\K{mem}}
.. |XTGLOBAL| mathdef:: \xref{syntax/types}{syntax-externtype}{\K{global}}
.. |XTTAG| mathdef:: \xref{syntax/types}{syntax-externtype}{\K{tag}}


.. Types, non-terminals

.. |numtype| mathdef:: \xref{syntax/types}{syntax-numtype}{\X{numtype}}
.. |packtype| mathdef:: \xref{syntax/types}{syntax-packtype}{\X{packtype}}
.. |lanetype| mathdef:: \xref{syntax/instructions}{syntax-lanetype}{\X{lanetype}}
.. |vectype| mathdef:: \xref{syntax/types}{syntax-vectype}{\X{vectype}}
.. |heaptype| mathdef:: \xref{syntax/types}{syntax-heaptype}{\X{heaptype}}
.. |absheaptype| mathdef:: \xref{syntax/types}{syntax-absheaptype}{\X{absheaptype}}
.. |reftype| mathdef:: \xref{syntax/types}{syntax-reftype}{\X{reftype}}
.. |consttype| mathdef:: \xref{syntax/types}{syntax-consttype}{\X{consttype}}
.. |valtype| mathdef:: \xref{syntax/types}{syntax-valtype}{\X{valtype}}
.. |resulttype| mathdef:: \xref{syntax/types}{syntax-resulttype}{\X{resulttype}}
.. |fieldtype| mathdef:: \xref{syntax/types}{syntax-fieldtype}{\X{fieldtype}}
.. |storagetype| mathdef:: \xref{syntax/types}{syntax-storagetype}{\X{storagetype}}
.. |comptype| mathdef:: \xref{syntax/types}{syntax-comptype}{\X{comptype}}
.. |subtype| mathdef:: \xref{syntax/types}{syntax-subtype}{\X{subtype}}
.. |rectype| mathdef:: \xref{syntax/types}{syntax-rectype}{\X{rectype}}
.. |deftype| mathdef:: \xref{valid/conventions}{syntax-deftype}{\X{deftype}}

.. |globaltype| mathdef:: \xref{syntax/types}{syntax-globaltype}{\X{globaltype}}
.. |tabletype| mathdef:: \xref{syntax/types}{syntax-tabletype}{\X{tabletype}}
.. |addrtype| mathdef:: \xref{syntax/types}{syntax-addrtype}{\X{addrtype}}
.. |memtype| mathdef:: \xref{syntax/types}{syntax-memtype}{\X{memtype}}
.. |tagtype| mathdef:: \xref{syntax/types}{syntax-tagtype}{\X{tagtype}}
.. |elemtype| mathdef:: \xref{syntax/types}{syntax-elemtype}{\X{elemtype}}
.. |datatype| mathdef:: \xref{syntax/types}{syntax-datatype}{\X{datatype}}
.. |externtype| mathdef:: \xref{syntax/types}{syntax-externtype}{\X{externtype}}

.. |limits| mathdef:: \xref{syntax/types}{syntax-limits}{\X{limits}}
.. |null| mathdef:: \xref{syntax/types}{syntax-null}{\X{null}}
.. |mut| mathdef:: \xref{syntax/types}{syntax-mut}{\X{mut}}
.. |final| mathdef:: \xref{syntax/types}{syntax-final}{\X{final}}
.. |init| mathdef:: \xref{valid/conventions}{syntax-init}{\X{init}}

.. |typeuse| mathdef:: \xref{syntax/types}{syntax-typeuse}{\X{typeuse}}

.. |instrtype| mathdef:: \xref{valid/conventions}{syntax-instrtype}{\X{instrtype}}
.. |localtype| mathdef:: \xref{valid/conventions}{syntax-localtype}{\X{localtype}}
.. |moduletype| mathdef:: \xref{valid/modules}{syntax-moduletype}{\X{moduletype}}


.. Types, meta functions

.. |addrtypemin| mathdef:: \xref{syntax/types}{aux-addrtype-min}{\F{min}}
.. |reftypediff| mathdef:: \xref{valid/conventions}{aux-reftypediff}{\setminus}

.. |rollrt| mathdef:: \xref{valid/conventions}{aux-roll-rectype}{\F{roll}}
.. |unrollrt| mathdef:: \xref{valid/conventions}{aux-unroll-rectype}{\F{unroll}}
.. |rolldt| mathdef:: \xref{valid/conventions}{aux-roll-deftype}{\F{roll}}
.. |unrolldt| mathdef:: \xref{valid/conventions}{aux-unroll-deftype}{\F{unroll}}
.. |expanddt| mathdef:: \xref{valid/conventions}{aux-expand-deftype}{\F{expand}}
.. |approxexpanddt| mathdef:: \mathrel{\xref{valid/conventions}{aux-expand-deftype}{\approx}}
.. |approxexpandyy| mathdef:: \mathrel{\xref{valid/conventions}{aux-expand-typeuse}{\approx}}
.. |unrollht| mathdef:: \xref{appendix/properties}{aux-unroll-heaptype}{\F{unroll}}

.. |unpack| mathdef:: \xref{syntax/types}{aux-unpack}{\F{unpack}}

.. |funcsxt| mathdef:: \xref{syntax/types}{syntax-externtype}{\F{funcs}}
.. |tablesxt| mathdef:: \xref{syntax/types}{syntax-externtype}{\F{tables}}
.. |memsxt| mathdef:: \xref{syntax/types}{syntax-externtype}{\F{mems}}
.. |globalsxt| mathdef:: \xref{syntax/types}{syntax-externtype}{\F{globals}}
.. |tagsxt| mathdef:: \xref{syntax/types}{syntax-externtype}{\F{tags}}

.. |assignsubst| mathdef:: \xref{valid/conventions}{notation-subst}{\mathrel{:=}}
.. |lbracksubst| mathdef:: \xref{valid/conventions}{notation-subst}{{[}}
.. |rbracksubst| mathdef:: \xref{valid/conventions}{notation-subst}{{]}}


.. Indices, non-terminals

.. |idx| mathdef:: \xref{syntax/modules}{syntax-idx}{\X{idx}}
.. |typeidx| mathdef:: \xref{syntax/modules}{syntax-typeidx}{\X{typeidx}}
.. |funcidx| mathdef:: \xref{syntax/modules}{syntax-funcidx}{\X{funcidx}}
.. |tableidx| mathdef:: \xref{syntax/modules}{syntax-tableidx}{\X{tableidx}}
.. |memidx| mathdef:: \xref{syntax/modules}{syntax-memidx}{\X{memidx}}
.. |globalidx| mathdef:: \xref{syntax/modules}{syntax-globalidx}{\X{globalidx}}
.. |tagidx| mathdef:: \xref{syntax/modules}{syntax-tagidx}{\X{tagidx}}
.. |elemidx| mathdef:: \xref{syntax/modules}{syntax-elemidx}{\X{elemidx}}
.. |dataidx| mathdef:: \xref{syntax/modules}{syntax-dataidx}{\X{dataidx}}
.. |localidx| mathdef:: \xref{syntax/modules}{syntax-localidx}{\X{localidx}}
.. |labelidx| mathdef:: \xref{syntax/modules}{syntax-labelidx}{\X{labelidx}}
.. |fieldidx| mathdef:: \xref{syntax/modules}{syntax-fieldidx}{\X{fieldidx}}

.. |externidx| mathdef:: \xref{syntax/modules}{syntax-externidx}{\X{externidx}}


.. Indices, meta functions

.. |freetypeidx| mathdef:: \xref{syntax/modules}{syntax-typeidx}{\F{typeidx}}
.. |freefuncidx| mathdef:: \xref{syntax/modules}{syntax-funcidx}{\F{funcidx}}
.. |freetableidx| mathdef:: \xref{syntax/modules}{syntax-tableidx}{\F{tableidx}}
.. |freememidx| mathdef:: \xref{syntax/modules}{syntax-memidx}{\F{memidx}}
.. |freeglobalidx| mathdef:: \xref{syntax/modules}{syntax-globalidx}{\F{globalidx}}
.. |freeelemidx| mathdef:: \xref{syntax/modules}{syntax-elemidx}{\F{elemidx}}
.. |freedataidx| mathdef:: \xref{syntax/modules}{syntax-dataidx}{\F{dataidx}}
.. |freelocalidx| mathdef:: \xref{syntax/modules}{syntax-localidx}{\F{localidx}}
.. |freelabelidx| mathdef:: \xref{syntax/modules}{syntax-labelidx}{\F{labelidx}}


.. Modules, terminals

.. |MODULE| mathdef:: \xref{syntax/modules}{syntax-module}{\K{module}}

.. |TYPE| mathdef:: \xref{syntax/modules}{syntax-type}{\K{type}}
.. |TAG| mathdef:: \xref{syntax/modules}{syntax-tag}{\K{tag}}
.. |GLOBAL| mathdef:: \xref{syntax/modules}{syntax-global}{\K{global}}
.. |MEMORY| mathdef:: \xref{syntax/modules}{syntax-mem}{\K{memory}}
.. |TABLE| mathdef:: \xref{syntax/modules}{syntax-table}{\K{table}}
.. |FUNC| mathdef:: \xref{syntax/modules}{syntax-func}{\K{func}}
.. |LOCAL| mathdef:: \xref{syntax/modules}{syntax-local}{\K{local}}
.. |ELEM| mathdef:: \xref{syntax/modules}{syntax-elem}{\K{elem}}
.. |DATA| mathdef:: \xref{syntax/modules}{syntax-data}{\K{data}}
.. |START| mathdef:: \xref{syntax/modules}{syntax-start}{\K{start}}
.. |IMPORT| mathdef:: \xref{syntax/modules}{syntax-import}{\K{import}}
.. |EXPORT| mathdef:: \xref{syntax/modules}{syntax-export}{\K{export}}

.. |DPASSIVE| mathdef:: \xref{syntax/modules}{syntax-datamode}{\K{passive}}
.. |DACTIVE| mathdef:: \xref{syntax/modules}{syntax-datamode}{\K{active}}

.. |EPASSIVE| mathdef:: \xref{syntax/modules}{syntax-elemmode}{\K{passive}}
.. |EACTIVE| mathdef:: \xref{syntax/modules}{syntax-elemmode}{\K{active}}
.. |EDECLARE| mathdef:: \xref{syntax/modules}{syntax-elemmode}{\K{declare}}

.. |XXFUNC| mathdef:: \xref{syntax/modules}{syntax-externidx}{\K{func}}
.. |XXTABLE| mathdef:: \xref{syntax/modules}{syntax-externidx}{\K{table}}
.. |XXMEM| mathdef:: \xref{syntax/modules}{syntax-externidx}{\K{memory}}
.. |XXGLOBAL| mathdef:: \xref{syntax/modules}{syntax-externidx}{\K{global}}
.. |XXTAG| mathdef:: \xref{syntax/modules}{syntax-externidx}{\K{tag}}


.. Modules, non-terminals

.. |module| mathdef:: \xref{syntax/modules}{syntax-module}{\X{module}}
.. |decl| mathdef:: \xref{text/modules}{syntax-decl}{\X{decl}}
.. |type| mathdef:: \xref{syntax/types}{syntax-rectype}{\X{type}}
.. |func| mathdef:: \xref{syntax/modules}{syntax-func}{\X{func}}
.. |local| mathdef:: \xref{syntax/modules}{syntax-local}{\X{local}}
.. |table| mathdef:: \xref{syntax/modules}{syntax-table}{\X{table}}
.. |mem| mathdef:: \xref{syntax/modules}{syntax-mem}{\X{mem}}
.. |global| mathdef:: \xref{syntax/modules}{syntax-global}{\X{global}}
.. |tag| mathdef:: \xref{syntax/modules}{syntax-tag}{\X{tag}}
.. |import| mathdef:: \xref{syntax/modules}{syntax-import}{\X{import}}
.. |export| mathdef:: \xref{syntax/modules}{syntax-export}{\X{export}}
.. |elem| mathdef:: \xref{syntax/modules}{syntax-elem}{\X{elem}}
.. |elemmode| mathdef:: \xref{syntax/modules}{syntax-elemmode}{\X{elemmode}}
.. |data| mathdef:: \xref{syntax/modules}{syntax-data}{\X{data}}
.. |datamode| mathdef:: \xref{syntax/modules}{syntax-datamode}{\X{datamode}}
.. |start| mathdef:: \xref{syntax/modules}{syntax-start}{\X{start}}


.. Modules, meta functions

.. |funcsxx| mathdef:: \xref{syntax/modules}{syntax-externidx}{\F{funcs}}
.. |tablesxx| mathdef:: \xref{syntax/modules}{syntax-externidx}{\F{tables}}
.. |memsxx| mathdef:: \xref{syntax/modules}{syntax-externidx}{\F{mems}}
.. |globalsxx| mathdef:: \xref{syntax/modules}{syntax-externidx}{\F{globals}}
.. |tagsxx| mathdef:: \xref{syntax/modules}{syntax-externidx}{\F{tags}}

.. |typesd| mathdef:: \xref{text/modules}{syntax-decl}{\F{types}}
.. |importsd| mathdef:: \xref{text/modules}{syntax-decl}{\F{imports}}
.. |tagsd| mathdef:: \xref{text/modules}{syntax-decl}{\F{tags}}
.. |globalsd| mathdef:: \xref{text/modules}{syntax-decl}{\F{globals}}
.. |memsd| mathdef:: \xref{text/modules}{syntax-decl}{\F{mems}}
.. |tablesd| mathdef:: \xref{text/modules}{syntax-decl}{\F{tables}}
.. |funcsd| mathdef:: \xref{text/modules}{syntax-decl}{\F{funcs}}
.. |datasd| mathdef:: \xref{text/modules}{syntax-decl}{\F{datas}}
.. |elemsd| mathdef:: \xref{text/modules}{syntax-decl}{\F{elems}}
.. |startsd| mathdef:: \xref{text/modules}{syntax-decl}{\F{starts}}
.. |exportsd| mathdef:: \xref{text/modules}{syntax-decl}{\F{exports}}

.. |ordered| mathdef:: \xref{text/modules}{aux-ordered}{\F{ordered}}


.. Instructions, terminals

.. |S| mathdef:: \xref{syntax/instructions}{syntax-sx}{\K{s}}
.. |U| mathdef:: \xref{syntax/instructions}{syntax-sx}{\K{u}}
.. |VS| mathdef:: \xref{syntax/instructions}{syntax-sx}{\K{s}}
.. |VU| mathdef:: \xref{syntax/instructions}{syntax-sx}{\K{u}}

.. |OFFSET| mathdef:: \xref{syntax/instructions}{syntax-instr-memory}{\K{offset}}
.. |ALIGN| mathdef:: \xref{syntax/instructions}{syntax-instr-memory}{\K{align}}

.. |Xshape| mathdef:: \xref{syntax/instructions}{syntax-shape}{\K{x}}

.. |UNREACHABLE| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{unreachable}}
.. |NOP| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{nop}}
.. |BLOCK| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{block}}
.. |LOOP| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{loop}}
.. |IF| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{if}}
.. |ELSE| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{else}}
.. |END| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{end}}
.. |BR| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{br}}
.. |BRIF| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{br\_if}}
.. |BRTABLE| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{br\_table}}
.. |BRONNULL| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{br\_on\_null}}
.. |BRONNONNULL| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{br\_on\_non\_null}}
.. |BRONCAST| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{br\_on\_cast}}
.. |BRONCASTFAIL| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{br\_on\_cast\_fail}}

.. |RETURN| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{return}}
.. |CALL| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{call}}
.. |CALLREF| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{call\_ref}}
.. |CALLINDIRECT| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{call\_indirect}}
.. |RETURNCALL| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{return\_call}}
.. |RETURNCALLREF| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{return\_call\_ref}}
.. |RETURNCALLINDIRECT| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{return\_call\_indirect}}

.. |THROW| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{throw}}
.. |THROWREF| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{throw\_ref}}
.. |TRYTABLE| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{try\_table}}
.. |CATCH| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{catch}}
.. |CATCHREF| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{catch\_ref}}
.. |CATCHALL| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{catch\_all}}
.. |CATCHALLREF| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{catch\_all\_ref}}

.. |DROP| mathdef:: \xref{syntax/instructions}{syntax-instr-parametric}{\K{drop}}
.. |SELECT| mathdef:: \xref{syntax/instructions}{syntax-instr-parametric}{\K{select}}

.. |LOCALGET| mathdef:: \xref{syntax/instructions}{syntax-instr-variable}{\K{local{.}get}}
.. |LOCALSET| mathdef:: \xref{syntax/instructions}{syntax-instr-variable}{\K{local{.}set}}
.. |LOCALTEE| mathdef:: \xref{syntax/instructions}{syntax-instr-variable}{\K{local{.}tee}}
.. |GLOBALGET| mathdef:: \xref{syntax/instructions}{syntax-instr-variable}{\K{global{.}get}}
.. |GLOBALSET| mathdef:: \xref{syntax/instructions}{syntax-instr-variable}{\K{global{.}set}}

.. |TABLEGET| mathdef:: \xref{syntax/instructions}{syntax-instr-table}{\K{table{.}get}}
.. |TABLESET| mathdef:: \xref{syntax/instructions}{syntax-instr-table}{\K{table{.}set}}
.. |TABLESIZE| mathdef:: \xref{syntax/instructions}{syntax-instr-table}{\K{table{.}size}}
.. |TABLEGROW| mathdef:: \xref{syntax/instructions}{syntax-instr-table}{\K{table{.}grow}}
.. |TABLEFILL| mathdef:: \xref{syntax/instructions}{syntax-instr-table}{\K{table{.}fill}}
.. |TABLECOPY| mathdef:: \xref{syntax/instructions}{syntax-instr-table}{\K{table{.}copy}}
.. |TABLEINIT| mathdef:: \xref{syntax/instructions}{syntax-instr-table}{\K{table{.}init}}
.. |ELEMDROP| mathdef:: \xref{syntax/instructions}{syntax-instr-table}{\K{elem{.}drop}}

.. |LOAD| mathdef:: \xref{syntax/instructions}{syntax-instr-memory}{\K{load}}
.. |STORE| mathdef:: \xref{syntax/instructions}{syntax-instr-memory}{\K{store}}
.. |VLOAD| mathdef:: \xref{syntax/instructions}{syntax-instr-memory}{\K{load}}
.. |VSTORE| mathdef:: \xref{syntax/instructions}{syntax-instr-memory}{\K{store}}
.. |VLANE| mathdef:: \xref{syntax/instructions}{syntax-instr-memory}{\K{lane}}
.. |MEMORYSIZE| mathdef:: \xref{syntax/instructions}{syntax-instr-memory}{\K{memory{.}size}}
.. |MEMORYGROW| mathdef:: \xref{syntax/instructions}{syntax-instr-memory}{\K{memory{.}grow}}
.. |MEMORYFILL| mathdef:: \xref{syntax/instructions}{syntax-instr-memory}{\K{memory{.}fill}}
.. |MEMORYCOPY| mathdef:: \xref{syntax/instructions}{syntax-instr-memory}{\K{memory{.}copy}}
.. |MEMORYINIT| mathdef:: \xref{syntax/instructions}{syntax-instr-memory}{\K{memory{.}init}}
.. |DATADROP| mathdef:: \xref{syntax/instructions}{syntax-instr-memory}{\K{data{.}drop}}

.. |LX| mathdef:: \xref{syntax/instructions}{syntax-instr-memory}{\K{x}}
.. |LSPLAT| mathdef:: \xref{syntax/instructions}{syntax-instr-memory}{\K{splat}}
.. |LZERO| mathdef:: \xref{syntax/instructions}{syntax-instr-memory}{\K{zero}}

.. |REFNULL| mathdef:: \xref{syntax/instructions}{syntax-instr-ref}{\K{ref{.}null}}
.. |REFFUNC| mathdef:: \xref{syntax/instructions}{syntax-instr-ref}{\K{ref{.}func}}
.. |REFISNULL| mathdef:: \xref{syntax/instructions}{syntax-instr-ref}{\K{ref{.}is\_null}}
.. |REFASNONNULL| mathdef:: \xref{syntax/instructions}{syntax-instr-ref}{\K{ref{.}as\_non\_null}}
.. |REFEQ| mathdef:: \xref{syntax/instructions}{syntax-instr-ref}{\K{ref{.}eq}}
.. |REFTEST| mathdef:: \xref{syntax/instructions}{syntax-instr-ref}{\K{ref{.}test}}
.. |REFCAST| mathdef:: \xref{syntax/instructions}{syntax-instr-ref}{\K{ref{.}cast}}

.. |STRUCTNEW| mathdef:: \xref{syntax/instructions}{syntax-instr-struct}{\K{struct{.}new}}
.. |STRUCTNEWDEFAULT| mathdef:: \xref{syntax/instructions}{syntax-instr-struct}{\K{struct{.}new\_default}}
.. |STRUCTGET| mathdef:: \xref{syntax/instructions}{syntax-instr-struct}{\K{struct{.}get}}
.. |STRUCTGETS| mathdef:: \xref{syntax/instructions}{syntax-instr-struct}{\K{struct{.}get\_s}}
.. |STRUCTGETU| mathdef:: \xref{syntax/instructions}{syntax-instr-struct}{\K{struct{.}get\_u}}
.. |STRUCTSET| mathdef:: \xref{syntax/instructions}{syntax-instr-struct}{\K{struct{.}set}}

.. |ARRAYNEW| mathdef:: \xref{syntax/instructions}{syntax-instr-array}{\K{array{.}new}}
.. |ARRAYNEWDEFAULT| mathdef:: \xref{syntax/instructions}{syntax-instr-array}{\K{array{.}new\_default}}
.. |ARRAYNEWFIXED| mathdef:: \xref{syntax/instructions}{syntax-instr-array}{\K{array{.}new\_fixed}}
.. |ARRAYNEWDATA| mathdef:: \xref{syntax/instructions}{syntax-instr-array}{\K{array{.}new\_data}}
.. |ARRAYNEWELEM| mathdef:: \xref{syntax/instructions}{syntax-instr-array}{\K{array{.}new\_elem}}
.. |ARRAYGET| mathdef:: \xref{syntax/instructions}{syntax-instr-array}{\K{array{.}get}}
.. |ARRAYGETS| mathdef:: \xref{syntax/instructions}{syntax-instr-array}{\K{array{.}get\_s}}
.. |ARRAYGETU| mathdef:: \xref{syntax/instructions}{syntax-instr-array}{\K{array{.}get\_u}}
.. |ARRAYSET| mathdef:: \xref{syntax/instructions}{syntax-instr-array}{\K{array{.}set}}
.. |ARRAYLEN| mathdef:: \xref{syntax/instructions}{syntax-instr-array}{\K{array{.}len}}
.. |ARRAYFILL| mathdef:: \xref{syntax/instructions}{syntax-instr-array}{\K{array{.}fill}}
.. |ARRAYCOPY| mathdef:: \xref{syntax/instructions}{syntax-instr-array}{\K{array{.}copy}}
.. |ARRAYINITDATA| mathdef:: \xref{syntax/instructions}{syntax-instr-array}{\K{array{.}init\_data}}
.. |ARRAYINITELEM| mathdef:: \xref{syntax/instructions}{syntax-instr-array}{\K{array{.}init\_elem}}

.. |REFI31| mathdef:: \xref{syntax/instructions}{syntax-instr-i31}{\K{ref{.}i\scriptstyle31}}
.. |I31GET| mathdef:: \xref{syntax/instructions}{syntax-instr-i31}{\K{i{\scriptstyle31}{.}get}}
.. |I31GETS| mathdef:: \xref{syntax/instructions}{syntax-instr-i31}{\K{i{\scriptstyle31}{.}get\_s}}
.. |I31GETU| mathdef:: \xref{syntax/instructions}{syntax-instr-i31}{\K{i{\scriptstyle31}{.}get\_u}}

.. |ANYCONVERTEXTERN| mathdef:: \xref{syntax/instructions}{syntax-instr-extern}{\K{any{.}convert\_extern}}
.. |EXTERNCONVERTANY| mathdef:: \xref{syntax/instructions}{syntax-instr-extern}{\K{extern{.}convert\_any}}

.. |CONST| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{const}}
.. |EQZ| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{eqz}}
.. |EQ| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{eq}}
.. |NE| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{ne}}
.. |LT| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{lt}}
.. |GT| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{gt}}
.. |LE| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{le}}
.. |GE| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{ge}}
.. |CLZ| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{clz}}
.. |CTZ| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{ctz}}
.. |POPCNT| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{popcnt}}
.. |ABS| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{abs}}
.. |NEG| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{neg}}
.. |CEIL| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{ceil}}
.. |FLOOR| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{floor}}
.. |TRUNC| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{trunc}}
.. |NEAREST| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{nearest}}
.. |SQRT| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{sqrt}}
.. |ADD| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{add}}
.. |SUB| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{sub}}
.. |MUL| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{mul}}
.. |DIV| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{div}}
.. |REM| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{rem}}
.. |FMIN| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{min}}
.. |FMAX| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{max}}
.. |AND| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{and}}
.. |OR| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{or}}
.. |XOR| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{xor}}
.. |SHL| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{shl}}
.. |SHR| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{shr}}
.. |ROTL| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{rotl}}
.. |ROTR| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{rotr}}
.. |COPYSIGN| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{copysign}}

.. |CONVERT| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{convert}}
.. |CONVERTSAT| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{convert\_sat}}
.. |TRUNCSAT| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{trunc\_sat}}
.. |EXTEND| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{extend}}
.. |WRAP| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{wrap}}
.. |PROMOTE| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{promote}}
.. |DEMOTE| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{demote}}
.. |REINTERPRET| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{reinterpret}}

.. |VCONST| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{const}}
.. |VSHUFFLE| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{shuffle}}
.. |VSWIZZLE| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{swizzle}}
.. |VSPLAT| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{splat}}
.. |VEXTRACTLANE| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{extract\_lane}}
.. |VREPLACELANE| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{replace\_lane}}
.. |VNOT| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{not}}
.. |VAND| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{and}}
.. |VANDNOT| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{andnot}}
.. |VOR| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{or}}
.. |VXOR| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{xor}}
.. |VBITSELECT| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{bitselect}}
.. |VEQ| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{eq}}
.. |VNE| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{ne}}
.. |VLT| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{lt}}
.. |VGT| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{gt}}
.. |VLE| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{le}}
.. |VGE| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{ge}}
.. |VABS| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{abs}}
.. |VNEG| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{neg}}
.. |VCEIL| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{ceil}}
.. |VFLOOR| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{floor}}
.. |VTRUNC| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{trunc}}
.. |VTRUNCSAT| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{trunc\_sat}}
.. |VNEAREST| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{nearest}}
.. |VPOPCNT| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{popcnt}}
.. |VANYTRUE| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{any\_true}}
.. |VALLTRUE| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{all\_true}}
.. |VBITMASK| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{bitmask}}
.. |VSHL| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{shl}}
.. |VSHR| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{shr}}
.. |VSQRT| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{sqrt}}
.. |VADD| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{add}}
.. |VSUB| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{sub}}
.. |VADDSAT| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{add\_sat}}
.. |VSUBSAT| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{sub\_sat}}
.. |VMUL| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{mul}}
.. |VDIV| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{div}}
.. |VMIN| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{min}}
.. |VMAX| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{max}}
.. |VPMIN| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{pmin}}
.. |VPMAX| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{pmax}}
.. |VNARROW| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{narrow}}
.. |VEXTEND| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{extend}}
.. |VAVGR| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{avgr}}
.. |VDOT| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{dot}}
.. |VEXTMUL| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{extmul}}
.. |VCONVERT| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{convert}}
.. |VQ15MULRSAT| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{q{\scriptstyle15}mulr\_sat}}
.. |VEXTADDPAIRWISE| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{extadd\_pairwise}}
.. |VDEMOTE| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{demote}}
.. |VPROMOTE| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{promote}}
.. |VRELAXEDMADD| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{relaxed\_madd}}
.. |VRELAXEDNMADD| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{relaxed\_nmadd}}
.. |VRELAXEDSWIZZLE| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{relaxed\_swizzle}}
.. |VRELAXEDLANESELECT| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{relaxed\_laneselect}}
.. |VRELAXEDMIN| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{relaxed\_min}}
.. |VRELAXEDMAX| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{relaxed\_max}}
.. |VRELAXEDQ15MULR| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{relaxed\_q15mulr}}
.. |VRELAXEDTRUNC| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{relaxed\_trunc}}
.. |VRELAXEDDOT| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{relaxed\_dot}}
.. |VRELAXEDDOTADD| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{relaxed\_dot\_add}}

.. |LOW| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{low}}
.. |HIGH| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{high}}
.. |ZERO| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{zero}}
.. |VLOW| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{low}}
.. |VHIGH| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{high}}
.. |VZERO| mathdef:: \xref{syntax/instructions}{syntax-instr-vec}{\K{zero}}


.. Instructions, non-terminals

.. |unop| mathdef:: \xref{syntax/instructions}{syntax-unop}{\X{unop}}
.. |binop| mathdef:: \xref{syntax/instructions}{syntax-binop}{\X{binop}}
.. |testop| mathdef:: \xref{syntax/instructions}{syntax-testop}{\X{testop}}
.. |relop| mathdef:: \xref{syntax/instructions}{syntax-relop}{\X{relop}}
.. |cvtop| mathdef:: \xref{syntax/instructions}{syntax-cvtop}{\X{cvtop}}

.. |unopF| mathdef:: \xref{exec/instructions}{exec-instr-numeric}{\X{unop}}
.. |binopF| mathdef:: \xref{exec/instructions}{exec-instr-numeric}{\X{binop}}
.. |testopF| mathdef:: \xref{exec/instructions}{exec-instr-numeric}{\X{testop}}
.. |relopF| mathdef:: \xref{exec/instructions}{exec-instr-numeric}{\X{relop}}
.. |cvtopF| mathdef:: \xref{exec/instructions}{exec-instr-numeric}{\X{cvtop}}

.. |iunop| mathdef:: \xref{syntax/instructions}{syntax-unop}{\X{iunop}}
.. |ibinop| mathdef:: \xref{syntax/instructions}{syntax-binop}{\X{ibinop}}
.. |itestop| mathdef:: \xref{syntax/instructions}{syntax-testop}{\X{itestop}}
.. |irelop| mathdef:: \xref{syntax/instructions}{syntax-relop}{\X{irelop}}

.. |funop| mathdef:: \xref{syntax/instructions}{syntax-unop}{\X{funop}}
.. |fbinop| mathdef:: \xref{syntax/instructions}{syntax-binop}{\X{fbinop}}
.. |ftestop| mathdef:: \xref{syntax/instructions}{syntax-testop}{\X{ftestop}}
.. |frelop| mathdef:: \xref{syntax/instructions}{syntax-relop}{\X{frelop}}

.. |dim| mathdef:: \xref{syntax/instructions}{syntax-dim}{\X{dim}}
.. |shape| mathdef:: \xref{syntax/instructions}{syntax-shape}{\X{shape}}
.. |ishape| mathdef:: \xref{syntax/instructions}{syntax-shape}{\X{ishape}}
.. |bshape| mathdef:: \xref{syntax/instructions}{syntax-shape}{\X{bshape}}

.. |vvunop| mathdef:: \xref{syntax/instructions}{syntax-vvunop}{\X{vvunop}}
.. |vvbinop| mathdef:: \xref{syntax/instructions}{syntax-vvbinop}{\X{vvbinop}}
.. |vvternop| mathdef:: \xref{syntax/instructions}{syntax-vvternop}{\X{vvternop}}
.. |vvtestop| mathdef:: \xref{syntax/instructions}{syntax-vvtestop}{\X{vvtestop}}

.. |vunop| mathdef:: \xref{syntax/instructions}{syntax-vunop}{\X{vunop}}
.. |vbinop| mathdef:: \xref{syntax/instructions}{syntax-vbinop}{\X{vbinop}}
.. |vternop| mathdef:: \xref{syntax/instructions}{syntax-vternop}{\X{vternop}}
.. |vtestop| mathdef:: \xref{syntax/instructions}{syntax-vrelop}{\X{vtestop}}
.. |vrelop| mathdef:: \xref{syntax/instructions}{syntax-vrelop}{\X{vrelop}}
.. |vcvtop| mathdef:: \xref{syntax/instructions}{syntax-vcvtop}{\X{vcvtop}}
.. |vextunop| mathdef:: \xref{syntax/instructions}{syntax-vextunop}{\X{vextunop}}
.. |vextbinop| mathdef:: \xref{syntax/instructions}{syntax-vextbinop}{\X{vextbinop}}
.. |vextternop| mathdef:: \xref{syntax/instructions}{syntax-vextternop}{\X{vextternop}}
.. |vbitmaskop| mathdef:: \xref{syntax/instructions}{syntax-vswizzlop}{\X{vbitmaskop}}
.. |vswizzlop| mathdef:: \xref{syntax/instructions}{syntax-vswizzlop}{\X{vswizzlop}}
.. |vshiftop| mathdef:: \xref{syntax/instructions}{syntax-vshiftop}{\X{vshiftop}}

.. |viunop| mathdef:: \xref{syntax/instructions}{syntax-vunop}{\X{viunop}}
.. |vibinop| mathdef:: \xref{syntax/instructions}{syntax-vbinop}{\X{vibinop}}
.. |vitestop| mathdef:: \xref{syntax/instructions}{syntax-vtestop}{\X{vitestop}}
.. |virelop| mathdef:: \xref{syntax/instructions}{syntax-vrelop}{\X{virelop}}
.. |viswizzlop| mathdef:: \xref{syntax/instructions}{syntax-vswizzlop}{\X{viswizzlop}}
.. |vishiftop| mathdef:: \xref{syntax/instructions}{syntax-vshiftop}{\X{vishiftop}}

.. |vfunop| mathdef:: \xref{syntax/instructions}{syntax-vunop}{\X{vfunop}}
.. |vfbinop| mathdef:: \xref{syntax/instructions}{syntax-vbinop}{\X{vfbinop}}
.. |vftestop| mathdef:: \xref{syntax/instructions}{syntax-vtestop}{\X{vftestop}}
.. |vfrelop| mathdef:: \xref{syntax/instructions}{syntax-vrelop}{\X{vfrelop}}

.. |loadop| mathdef:: \xref{syntax/instructions}{syntax-loadop}{\X{loadop}}
.. |storeop| mathdef:: \xref{syntax/instructions}{syntax-storeop}{\X{storeop}}
.. |vloadop| mathdef:: \xref{syntax/instructions}{syntax-vloadop}{\X{vloadop}}

.. |sx| mathdef:: \xref{syntax/instructions}{syntax-sx}{\X{sx}}
.. |sz| mathdef:: \xref{syntax/instructions}{syntax-sz}{\X{sz}}
.. |half| mathdef:: \xref{syntax/instructions}{syntax-half}{\X{half}}
.. |zero| mathdef:: \xref{syntax/instructions}{syntax-zero}{\X{zero}}
.. |memarg| mathdef:: \xref{syntax/instructions}{syntax-memarg}{\X{memarg}}
.. |laneidx| mathdef:: \xref{syntax/instructions}{syntax-laneidx}{\X{laneidx}}

.. |blocktype| mathdef:: \xref{syntax/types}{syntax-blocktype}{\X{blocktype}}

.. |instr| mathdef:: \xref{syntax/instructions}{syntax-instr}{\X{instr}}
.. |catch| mathdef:: \xref{syntax/instructions}{syntax-catch}{\X{catch}}
.. |expr| mathdef:: \xref{syntax/instructions}{syntax-expr}{\X{expr}}



.. Binary Format
.. -------------

.. Auxiliary productions

.. |Blist| mathdef:: \xref{binary/conventions}{binary-list}{\B{list}}


.. Values, non-terminals

.. |Bbyte| mathdef:: \xref{binary/values}{binary-byte}{\B{byte}}

.. |BuX#1| mathdef:: {\B{u}#1}
.. |BsX#1| mathdef:: {\B{s}#1}
.. |BiX#1| mathdef:: {\B{i}#1}
.. |BfX#1| mathdef:: {\B{f}#1}

.. |BuNX| mathdef:: \xref{binary/values}{binary-int}{\BuX{}}
.. |BuN| mathdef:: \xref{binary/values}{binary-int}{\BuX{\scriptstyle N}}
.. |Bu1| mathdef:: \xref{binary/values}{binary-int}{\BuX{\B{1}}}
.. |Bu8| mathdef:: \xref{binary/values}{binary-int}{\BuX{\B{8}}}
.. |Bu16| mathdef:: \xref{binary/values}{binary-int}{\BuX{\B{16}}}
.. |Bu32| mathdef:: \xref{binary/values}{binary-int}{\BuX{\B{32}}}
.. |Bu64| mathdef:: \xref{binary/values}{binary-int}{\BuX{\B{64}}}

.. |BsNX| mathdef:: \xref{binary/values}{binary-int}{\BsX{}}
.. |BsN| mathdef:: \xref{binary/values}{binary-int}{\BsX{\scriptstyle N}}
.. |Bs7| mathdef:: \xref{binary/values}{binary-int}{\BsX{\B{7}}}
.. |Bs32| mathdef:: \xref{binary/values}{binary-int}{\BsX{\B{32}}}
.. |Bs33| mathdef:: \xref{binary/values}{binary-int}{\BsX{\B{33}}}
.. |Bs64| mathdef:: \xref{binary/values}{binary-int}{\BsX{\B{64}}}

.. |BiNX| mathdef:: \xref{binary/values}{binary-int}{\BiX{}}
.. |BiN| mathdef:: \xref{binary/values}{binary-int}{\BiX{\scriptstyle N}}
.. |Bi32| mathdef:: \xref{binary/values}{binary-int}{\BiX{\B{32}}}
.. |Bi64| mathdef:: \xref{binary/values}{binary-int}{\BiX{\B{64}}}

.. |BfNX| mathdef:: \xref{binary/values}{binary-float}{\BfX{}}
.. |BfN| mathdef:: \xref{binary/values}{binary-float}{\BfX{\scriptstyle N}}
.. |Bf32| mathdef:: \xref{binary/values}{binary-float}{\BfX{\B{32}}}
.. |Bf64| mathdef:: \xref{binary/values}{binary-float}{\BfX{\B{64}}}

.. |Bname| mathdef:: \xref{binary/values}{binary-name}{\B{name}}


.. Values, meta functions

.. |utf8| mathdef:: \xref{binary/values}{binary-utf8}{\F{utf\scriptstyle8}}


.. Types, non-terminals

.. |Bnumtype| mathdef:: \xref{binary/types}{binary-numtype}{\B{numtype}}
.. |Bvectype| mathdef:: \xref{binary/types}{binary-vectype}{\B{vectype}}
.. |Bheaptype| mathdef:: \xref{binary/types}{binary-heaptype}{\B{heaptype}}
.. |Babsheaptype| mathdef:: \xref{binary/types}{binary-absheaptype}{\B{absheaptype}}
.. |Breftype| mathdef:: \xref{binary/types}{binary-reftype}{\B{reftype}}
.. |Bvaltype| mathdef:: \xref{binary/types}{binary-valtype}{\B{valtype}}
.. |Bresulttype| mathdef:: \xref{binary/types}{binary-resulttype}{\B{resulttype}}
.. |Bfieldtype| mathdef:: \xref{binary/types}{binary-fieldtype}{\B{fieldtype}}
.. |Bstoragetype| mathdef:: \xref{binary/types}{binary-storagetype}{\B{storagetype}}
.. |Bpacktype| mathdef:: \xref{binary/types}{binary-packtype}{\B{packtype}}
.. |Bcomptype| mathdef:: \xref{binary/types}{binary-comptype}{\B{comptype}}
.. |Bsubtype| mathdef:: \xref{binary/types}{binary-subtype}{\B{subtype}}
.. |Brectype| mathdef:: \xref{binary/types}{binary-rectype}{\B{rectype}}
.. |Bglobaltype| mathdef:: \xref{binary/types}{binary-globaltype}{\B{globaltype}}
.. |Btagtype| mathdef:: \xref{binary/types}{binary-tagtype}{\B{tagtype}}
.. |Btabletype| mathdef:: \xref{binary/types}{binary-tabletype}{\B{tabletype}}
.. |Bmemtype| mathdef:: \xref{binary/types}{binary-memtype}{\B{memtype}}
.. |Blimits| mathdef:: \xref{binary/types}{binary-limits}{\B{limits}}
.. |Bmut| mathdef:: \xref{binary/types}{binary-mut}{\B{mut}}
.. |Bexterntype| mathdef:: \xref{binary/types}{binary-externtype}{\B{externtype}}


.. Indices, non-terminals

.. |Bidx| mathdef:: \xref{binary/modules}{binary-index}{\B{idx}}
.. |Btypeidx| mathdef:: \xref{binary/modules}{binary-typeidx}{\B{typeidx}}
.. |Bfuncidx| mathdef:: \xref{binary/modules}{binary-funcidx}{\B{funcidx}}
.. |Btableidx| mathdef:: \xref{binary/modules}{binary-tableidx}{\B{tableidx}}
.. |Bmemidx| mathdef:: \xref{binary/modules}{binary-memidx}{\B{memidx}}
.. |Bglobalidx| mathdef:: \xref{binary/modules}{binary-globalidx}{\B{globalidx}}
.. |Btagidx| mathdef:: \xref{binary/modules}{binary-tagidx}{\B{tagidx}}
.. |Belemidx| mathdef:: \xref{binary/modules}{binary-elemidx}{\B{elemidx}}
.. |Bdataidx| mathdef:: \xref{binary/modules}{binary-dataidx}{\B{dataidx}}
.. |Blocalidx| mathdef:: \xref{binary/modules}{binary-localidx}{\B{localidx}}
.. |Blabelidx| mathdef:: \xref{binary/modules}{binary-labelidx}{\B{labelidx}}
.. |Bfieldidx| mathdef:: \xref{binary/modules}{binary-fieldidx}{\B{fieldidx}}

.. |Bexternidx| mathdef:: \xref{binary/modules}{binary-externidx}{\B{externidx}}


.. Modules, non-terminals

.. |Bmagic| mathdef:: \xref{binary/modules}{binary-magic}{\B{magic}}
.. |Bversion| mathdef:: \xref{binary/modules}{binary-version}{\B{version}}
.. |Bmodule| mathdef:: \xref{binary/modules}{binary-module}{\B{module}}

.. |Bsection| mathdef:: \xref{binary/modules}{binary-section}{\B{section}}
.. |Bcustomsec| mathdef:: \xref{binary/modules}{binary-customsec}{\B{customsec}}
.. |Btypesec| mathdef:: \xref{binary/modules}{binary-typesec}{\B{typesec}}
.. |Bfuncsec| mathdef:: \xref{binary/modules}{binary-funcsec}{\B{funcsec}}
.. |Bcodesec| mathdef:: \xref{binary/modules}{binary-codesec}{\B{codesec}}
.. |Btablesec| mathdef:: \xref{binary/modules}{binary-tablesec}{\B{tablesec}}
.. |Bmemsec| mathdef:: \xref{binary/modules}{binary-memsec}{\B{memsec}}
.. |Bglobalsec| mathdef:: \xref{binary/modules}{binary-globalsec}{\B{globalsec}}
.. |Btagsec| mathdef:: \xref{binary/modules}{binary-tagsec}{\B{tagsec}}
.. |Bimportsec| mathdef:: \xref{binary/modules}{binary-importsec}{\B{importsec}}
.. |Bexportsec| mathdef:: \xref{binary/modules}{binary-exportsec}{\B{exportsec}}
.. |Belemsec| mathdef:: \xref{binary/modules}{binary-elemsec}{\B{elemsec}}
.. |Bdatasec| mathdef:: \xref{binary/modules}{binary-datasec}{\B{datasec}}
.. |Bstartsec| mathdef:: \xref{binary/modules}{binary-startsec}{\B{startsec}}
.. |Bdatacntsec| mathdef:: \xref{binary/modules}{binary-datacntsec}{\B{datacntsec}}

.. |Bcustom| mathdef:: \xref{binary/modules}{binary-customsec}{\B{custom}}
.. |Btype| mathdef:: \xref{binary/modules}{binary-type}{\B{type}}
.. |Bfunc| mathdef:: \xref{binary/modules}{binary-func}{\B{func}}
.. |Btable| mathdef:: \xref{binary/modules}{binary-table}{\B{table}}
.. |Bmem| mathdef:: \xref{binary/modules}{binary-mem}{\B{mem}}
.. |Bglobal| mathdef:: \xref{binary/modules}{binary-global}{\B{global}}
.. |Btag| mathdef:: \xref{binary/modules}{binary-tag}{\B{tag}}
.. |Bimport| mathdef:: \xref{binary/modules}{binary-import}{\B{import}}
.. |Bexport| mathdef:: \xref{binary/modules}{binary-export}{\B{export}}
.. |Belem| mathdef:: \xref{binary/modules}{binary-elem}{\B{elem}}
.. |Belemkind| mathdef:: \xref{binary/modules}{binary-elemkind}{\B{elemkind}}
.. |Bcode| mathdef:: \xref{binary/modules}{binary-code}{\B{code}}
.. |Blocal| mathdef:: \xref{binary/modules}{binary-local}{\B{local}}
.. |Blocals| mathdef:: \xref{binary/modules}{binary-local}{\B{locals}}
.. |Bdata| mathdef:: \xref{binary/modules}{binary-data}{\B{data}}
.. |Bstart| mathdef:: \xref{binary/modules}{binary-start}{\B{start}}
.. |Bdatacnt| mathdef:: \xref{binary/modules}{binary-datacnt}{\B{datacnt}}


.. Instructions, non-terminals

.. |Bmemarg| mathdef:: \xref{binary/instructions}{binary-memarg}{\B{memarg}}
.. |Bblocktype| mathdef:: \xref{binary/instructions}{binary-blocktype}{\B{blocktype}}
.. |Bcastop| mathdef:: \xref{binary/instructions}{binary-castop}{\B{castop}}

.. |Binstr| mathdef:: \xref{binary/instructions}{binary-instr}{\B{instr}}
.. |Bcatch| mathdef:: \xref{binary/instructions}{binary-catch}{\B{catch}}
.. |Bexpr| mathdef:: \xref{binary/instructions}{binary-expr}{\B{expr}}

.. |Blaneidx| mathdef:: \xref{binary/instructions}{binary-laneidx}{\B{laneidx}}


.. Text Format
.. -----------

.. Auxiliary productions

.. |Tlist| mathdef:: \xref{text/conventions}{text-list}{\T{list}}


.. Lexical grammar, terminals

.. |textl| mathdef:: \mbox{‘}
.. |textr| mathdef:: \mbox{’}
.. |text#1| mathdef:: \textl\mathtt{#1}\textr

.. |Tcommentl| mathdef:: \text{{(}{;}}
.. |Tcommentr| mathdef:: \text{{;}{)}}
.. |Tcommentd| mathdef:: \text{{;}{;}}


.. Lexical grammar, non-terminals

.. |Tsource| mathdef:: \xref{text/lexical}{text-source}{\T{source}}
.. |Tchar| mathdef:: \xref{text/lexical}{text-char}{\T{char}}
.. |Tspace| mathdef:: \xref{text/lexical}{text-space}{\T{space}}
.. |Tformat| mathdef:: \xref{text/lexical}{text-format}{\T{format}}
.. |Tnewline| mathdef:: \xref{text/lexical}{text-newline}{\T{newline}}

.. |Ttoken| mathdef:: \xref{text/lexical}{text-token}{\T{token}}
.. |Tkeyword| mathdef:: \xref{text/lexical}{text-keyword}{\T{keyword}}
.. |Treserved| mathdef:: \xref{text/lexical}{text-reserved}{\T{reserved}}

.. |Teof| mathdef:: \xref{text/lexical}{text-eof}{\T{eof}}

.. |Tcomment| mathdef:: \xref{text/lexical}{text-comment}{\T{comment}}
.. |Tlinecomment| mathdef:: \xref{text/lexical}{text-comment}{\T{linecomment}}
.. |Tblockcomment| mathdef:: \xref{text/lexical}{text-comment}{\T{blockcomment}}
.. |Tlinechar| mathdef:: \xref{text/lexical}{text-comment}{\T{linechar}}
.. |Tblockchar| mathdef:: \xref{text/lexical}{text-comment}{\T{blockchar}}

.. |Tannot| mathdef:: \xref{text/lexical}{text-annot}{\T{annot}}
.. |Tannotid| mathdef:: \xref{text/lexical}{text-annot}{\T{annotid}}
.. |Tannottoken| mathdef:: \xref{text/lexical}{text-annot}{\T{annottoken}}


.. Values, non-terminals

.. |Tsign| mathdef:: \xref{text/values}{text-sign}{\T{sign}}
.. |Tdigit| mathdef:: \xref{text/values}{text-digit}{\T{digit}}
.. |Thexdigit| mathdef:: \xref{text/values}{text-hexdigit}{\T{hexdigit}}
.. |Tnum| mathdef:: \xref{text/values}{text-num}{\T{num}}
.. |Thexnum| mathdef:: \xref{text/values}{text-hexnum}{\T{hexnum}}
.. |Tfrac| mathdef:: \xref{text/values}{text-frac}{\T{frac}}
.. |Thexfrac| mathdef:: \xref{text/values}{text-hexfrac}{\T{hexfrac}}
.. |Tmant| mathdef:: \xref{text/values}{text-mant}{\T{mant}}
.. |Thexmant| mathdef:: \xref{text/values}{text-hexmant}{\T{hexmant}}
.. |Tfloat| mathdef:: \xref{text/values}{text-float}{\T{float}}
.. |Thexfloat| mathdef:: \xref{text/values}{text-hexfloat}{\T{hexfloat}}

.. |TuNX| mathdef:: \xref{text/values}{text-int}{\T{u}\kern-0.1em}
.. |TsNX| mathdef:: \xref{text/values}{text-int}{\T{s}\kern-0.1em}
.. |TiNX| mathdef:: \xref{text/values}{text-int}{\T{i}\kern-0.1em}
.. |TfNX| mathdef:: \xref{text/values}{text-int}{\T{f}\kern-0.1em}

.. |TuX#1| mathdef:: {\T{u}#1}
.. |TsX#1| mathdef:: {\T{s}#1}
.. |TiX#1| mathdef:: {\T{i}#1}
.. |TfX#1| mathdef:: {\T{f}#1}

.. |TuN| mathdef:: \xref{text/values}{text-int}{\TuX{{\kern-0.1em N}}}
.. |Tu1| mathdef:: \xref{text/values}{text-int}{\T{u1}}
.. |Tu8| mathdef:: \xref{text/values}{text-int}{\T{u8}}
.. |Tu16| mathdef:: \xref{text/values}{text-int}{\T{u16}}
.. |Tu32| mathdef:: \xref{text/values}{text-int}{\T{u32}}
.. |Tu64| mathdef:: \xref{text/values}{text-int}{\T{u64}}

.. |TsN| mathdef:: \xref{text/values}{text-int}{\TsX{\kern-0.1em N}}
.. |Ts32| mathdef:: \xref{text/values}{text-int}{\T{s32}}
.. |Ts64| mathdef:: \xref{text/values}{text-int}{\T{s64}}

.. |TiN| mathdef:: \xref{text/values}{text-int}{\TiX{\kern-0.1em N}}
.. |Ti8| mathdef:: \xref{text/values}{text-int}{\T{i8}}
.. |Ti16| mathdef:: \xref{text/values}{text-int}{\T{i16}}
.. |Ti32| mathdef:: \xref{text/values}{text-int}{\T{i32}}
.. |Ti64| mathdef:: \xref{text/values}{text-int}{\T{i64}}

.. |TfN| mathdef:: \xref{text/values}{text-float}{\TfX{\kern-0.1em N}}
.. |TfNmag| mathdef:: \xref{text/values}{text-float}{\TfX{N}\T{mag}}
.. |Tf32| mathdef:: \xref{text/values}{text-float}{\T{f32}}
.. |Tf64| mathdef:: \xref{text/values}{text-float}{\T{f64}}

.. |Tstring| mathdef:: \xref{text/values}{text-string}{\T{string}}
.. |Tstringelem| mathdef:: \xref{text/values}{text-string}{\T{stringelem}}
.. |Tstringchar| mathdef:: \xref{text/values}{text-string}{\T{stringchar}}
.. |Tname| mathdef:: \xref{text/values}{text-name}{\T{name}}

.. |Tid| mathdef:: \xref{text/values}{text-id}{\T{id}}
.. |Tidchar| mathdef:: \xref{text/values}{text-idchar}{\T{idchar}}


.. Types, non-terminals

.. |Tnull| mathdef:: \xref{text/types}{text-null}{\T{null}}
.. |Tfinal| mathdef:: \xref{text/types}{text-final}{\T{final}}

.. |Tnumtype| mathdef:: \xref{text/types}{text-numtype}{\T{numtype}}
.. |Tvectype| mathdef:: \xref{text/types}{text-vectype}{\T{vectype}}
.. |Theaptype| mathdef:: \xref{text/types}{text-heaptype}{\T{heaptype}}
.. |Tabsheaptype| mathdef:: \xref{text/types}{text-absheaptype}{\T{absheaptype}}
.. |Treftype| mathdef:: \xref{text/types}{text-reftype}{\T{reftype}}
.. |Tvaltype| mathdef:: \xref{text/types}{text-valtype}{\T{valtype}}
.. |Taggrtype| mathdef:: \xref{text/types}{text-aggrtype}{\T{aggrtype}}
.. |Tfieldtype| mathdef:: \xref{text/types}{text-fieldtype}{\T{fieldtype}}
.. |Tstoragetype| mathdef:: \xref{text/types}{text-storagetype}{\T{storagetype}}
.. |Tpacktype| mathdef:: \xref{text/types}{text-packtype}{\T{packtype}}
.. |Tcomptype| mathdef:: \xref{text/types}{text-comptype}{\T{comptype}}
.. |Tsubtype| mathdef:: \xref{text/types}{text-subtype}{\T{subtype}}
.. |Ttypedef| mathdef:: \xref{text/types}{text-typedef}{\T{typedef}}
.. |Trectype| mathdef:: \xref{text/types}{text-rectype}{\T{rectype}}

.. |Texterntype| mathdef:: \xref{text/types}{text-externtype}{\T{externtype}}
.. |Ttagtype| mathdef:: \xref{text/types}{text-tagtype}{\T{tagtype}}
.. |Tglobaltype| mathdef:: \xref{text/types}{text-globaltype}{\T{globaltype}}
.. |Ttabletype| mathdef:: \xref{text/types}{text-tabletype}{\T{tabletype}}
.. |Taddrtype| mathdef:: \xref{text/types}{text-addrtype}{\T{addrtype}}
.. |Tmemtype| mathdef:: \xref{text/types}{text-memtype}{\T{memtype}}
.. |Tlimits| mathdef:: \xref{text/types}{text-limits}{\T{limits}}

.. |Tparam| mathdef:: \xref{text/types}{text-comptype}{\T{param}}
.. |Tresult| mathdef:: \xref{text/types}{text-comptype}{\T{result}}
.. |Tfield| mathdef:: \xref{text/types}{text-comptype}{\T{field}}


.. Indices, non-terminals

.. |Tidx| mathdef:: \xref{text/modules}{text-idx}{\T{idx}}
.. |Ttypeidx| mathdef:: \xref{text/modules}{text-typeidx}{\T{typeidx}}
.. |Tfuncidx| mathdef:: \xref{text/modules}{text-funcidx}{\T{funcidx}}
.. |Ttableidx| mathdef:: \xref{text/modules}{text-tableidx}{\T{tableidx}}
.. |Tmemidx| mathdef:: \xref{text/modules}{text-memidx}{\T{memidx}}
.. |Tglobalidx| mathdef:: \xref{text/modules}{text-globalidx}{\T{globalidx}}
.. |Ttagidx| mathdef:: \xref{text/modules}{text-tagidx}{\T{tagidx}}
.. |Telemidx| mathdef:: \xref{text/modules}{text-elemidx}{\T{elemidx}}
.. |Tdataidx| mathdef:: \xref{text/modules}{text-dataidx}{\T{dataidx}}
.. |Tlocalidx| mathdef:: \xref{text/modules}{text-localidx}{\T{localidx}}
.. |Tlabelidx| mathdef:: \xref{text/modules}{text-labelidx}{\T{labelidx}}
.. |Tfieldidx| mathdef:: \xref{text/modules}{text-fieldidx}{\T{fieldidx}}


.. Modules, non-terminals

.. |Tmodule| mathdef:: \xref{text/modules}{text-module}{\T{module}}
.. |Tdecl| mathdef:: \xref{text/modules}{text-decl}{\T{decl}}
.. |Ttype| mathdef:: \xref{text/types}{text-type}{\T{type}}
.. |Ttypeuse| mathdef:: \xref{text/types}{text-typeuse}{\T{typeuse}}
.. |Tfunc| mathdef:: \xref{text/modules}{text-func}{\T{func}}
.. |Ttable| mathdef:: \xref{text/modules}{text-table}{\T{table}}
.. |Tmem| mathdef:: \xref{text/modules}{text-mem}{\T{mem}}
.. |Tglobal| mathdef:: \xref{text/modules}{text-global}{\T{global}}
.. |Ttag| mathdef:: \xref{text/modules}{text-tag}{\T{tag}}
.. |Timport| mathdef:: \xref{text/modules}{text-import}{\T{import}}
.. |Texport| mathdef:: \xref{text/modules}{text-export}{\T{export}}
.. |Texternidx| mathdef:: \xref{text/modules}{text-externidx}{\T{externidx}}
.. |Telem| mathdef:: \xref{text/modules}{text-elem}{\T{elem}}
.. |Telemlist| mathdef:: \xref{text/modules}{text-elemlist}{\T{elemlist}}
.. |Telemexpr| mathdef:: \xref{text/modules}{text-elemexpr}{\T{elemexpr}}
.. |Ttableuse| mathdef:: \xref{text/modules}{text-tableuse}{\T{tableuse}}
.. |Tlocal| mathdef:: \xref{text/modules}{text-local}{\T{local}}
.. |Tlocals| mathdef:: \xref{text/modules}{text-local}{\T{locals}}
.. |Tdata| mathdef:: \xref{text/modules}{text-data}{\T{data}}
.. |Tdatastring| mathdef:: \xref{text/modules}{text-datastring}{\T{datastring}}
.. |Tmemuse| mathdef:: \xref{text/modules}{text-memuse}{\T{memuse}}
.. |Tstart| mathdef:: \xref{text/modules}{text-start}{\T{start}}


.. Instructions, non-terminals

.. |Tmemarg| mathdef:: \xref{text/instructions}{text-memarg}{\T{memarg}}
.. |Talign| mathdef:: \xref{text/instructions}{text-memarg}{\T{align}}
.. |Toffset| mathdef:: \xref{text/instructions}{text-memarg}{\T{offset}}
.. |Tlaneidx| mathdef:: \xref{text/instructions}{text-laneidx}{\T{laneidx}}

.. |Tblocktype| mathdef:: \xref{text/instructions}{text-blocktype}{\T{blocktype}}

.. |Tlabel| mathdef:: \xref{text/instructions}{text-label}{\T{label}}
.. |Tinstr| mathdef:: \xref{text/instructions}{text-instr}{\T{instr}}
.. |Tinstrs| mathdef:: \xref{text/instructions}{text-instrs}{\T{instrs}}
.. |Tplaininstr| mathdef:: \xref{text/instructions}{text-plaininstr}{\T{plaininstr}}
.. |Tblockinstr| mathdef:: \xref{text/instructions}{text-blockinstr}{\T{blockinstr}}
.. |Tfoldedinstr| mathdef:: \xref{text/instructions}{text-foldedinstr}{\T{foldedinstr}}
.. |Tcatch| mathdef:: \xref{text/instructions}{text-catch}{\T{catch}}
.. |Texpr| mathdef:: \xref{text/instructions}{text-expr}{\T{expr}}



.. Parsing
.. -------

.. Contexts

.. |I| mathdef:: \xref{text/conventions}{text-context}{I}

.. |ITYPEDEFS| mathdef:: \xref{text/conventions}{text-context}{\K{typedefs}}
.. |IFIELDS| mathdef:: \xref{text/conventions}{text-context}{\K{fields}}
.. |ITYPES| mathdef:: \xref{text/conventions}{text-context}{\K{types}}
.. |IFUNCS| mathdef:: \xref{text/conventions}{text-context}{\K{funcs}}
.. |ITABLES| mathdef:: \xref{text/conventions}{text-context}{\K{tables}}
.. |IMEMS| mathdef:: \xref{text/conventions}{text-context}{\K{mems}}
.. |IGLOBALS| mathdef:: \xref{text/conventions}{text-context}{\K{globals}}
.. |ITAGS| mathdef:: \xref{text/conventions}{text-context}{\K{tags}}
.. |IELEMS| mathdef:: \xref{text/conventions}{text-context}{\K{elems}}
.. |IDATAS| mathdef:: \xref{text/conventions}{text-context}{\K{datas}}
.. |ILOCALS| mathdef:: \xref{text/conventions}{text-context}{\K{locals}}
.. |ILABELS| mathdef:: \xref{text/conventions}{text-context}{\K{labels}}


.. Meta Functions

.. |idfresh| mathdef:: ~\xref{text/values}{text-id-fresh}{\mbox{fresh}}
.. |idcwellformed| mathdef:: ~\xref{text/conventions}{text-context-wf}{\mbox{well-formed}}




.. Validation
.. ----------

.. Meta functions

.. |clostype| mathdef:: \xref{valid/conventions}{aux-clostype}{\K{clos}}


.. Contexts

.. |context| mathdef:: \xref{valid/conventions}{context}{\X{context}}
.. |C| mathdef:: \xref{valid/conventions}{context}{C}

.. |CTYPES| mathdef:: \xref{valid/conventions}{context}{\K{types}}
.. |CFUNCS| mathdef:: \xref{valid/conventions}{context}{\K{funcs}}
.. |CTABLES| mathdef:: \xref{valid/conventions}{context}{\K{tables}}
.. |CMEMS| mathdef:: \xref{valid/conventions}{context}{\K{mems}}
.. |CGLOBALS| mathdef:: \xref{valid/conventions}{context}{\K{globals}}
.. |CTAGS| mathdef:: \xref{valid/conventions}{context}{\K{tags}}
.. |CELEMS| mathdef:: \xref{valid/conventions}{context}{\K{elems}}
.. |CDATAS| mathdef:: \xref{valid/conventions}{context}{\K{datas}}
.. |CLOCALS| mathdef:: \xref{valid/conventions}{context}{\K{locals}}
.. |CLABELS| mathdef:: \xref{valid/conventions}{context}{\K{labels}}
.. |CRETURN| mathdef:: \xref{valid/conventions}{context}{\K{return}}
.. |CREFS| mathdef:: \xref{valid/conventions}{context}{\K{refs}}
.. |CRECS| mathdef:: \xref{appendix/properties}{context-ext}{\K{recs}}


.. Judgments

.. |vdashnumtype| mathdef:: \xref{valid/types}{valid-numtype}{\vdash}
.. |vdashvectype| mathdef:: \xref{valid/types}{valid-vectype}{\vdash}
.. |vdashheaptype| mathdef:: \xref{valid/types}{valid-heaptype}{\vdash}
.. |vdashreftype| mathdef:: \xref{valid/types}{valid-reftype}{\vdash}
.. |vdashvaltype| mathdef:: \xref{valid/types}{valid-valtype}{\vdash}
.. |vdashresulttype| mathdef:: \xref{valid/types}{valid-resulttype}{\vdash}
.. |vdashlimits| mathdef:: \xref{valid/types}{valid-limits}{\vdash}
.. |vdashblocktype| mathdef:: \xref{valid/types}{valid-blocktype}{\vdash}
.. |vdashcomptype| mathdef:: \xref{valid/types}{valid-comptype}{\vdash}
.. |vdashfieldtype| mathdef:: \xref{valid/types}{valid-fieldtype}{\vdash}
.. |vdashpacktype| mathdef:: \xref{valid/types}{valid-packtype}{\vdash}
.. |vdashstoragetype| mathdef:: \xref{valid/types}{valid-storagetype}{\vdash}
.. |vdashsubtype| mathdef:: \xref{valid/types}{valid-subtype}{\vdash}
.. |vdashsubtypeext| mathdef:: \xref{valid/types}{valid-subtype}{\vdash}
.. |vdashrectype| mathdef:: \xref{valid/types}{valid-rectype}{\vdash}
.. |vdashrectypeext| mathdef:: \xref{valid/types}{valid-rectype}{\vdash}
.. |vdashtabletype| mathdef:: \xref{valid/types}{valid-tabletype}{\vdash}
.. |vdashmemtype| mathdef:: \xref{valid/types}{valid-memtype}{\vdash}
.. |vdashglobaltype| mathdef:: \xref{valid/types}{valid-globaltype}{\vdash}
.. |vdashlocaltype| mathdef:: \xref{appendix/properties}{valid-localtype}{\vdash}
.. |vdashtagtype| mathdef:: \xref{valid/types}{valid-tagtype}{\vdash}
.. |vdashexterntype| mathdef:: \xref{valid/types}{valid-externtype}{\vdash}
.. |vdashdeftype| mathdef:: \xref{appendix/properties}{valid-deftype}{\vdash}
.. |vdashtypeuse| mathdef:: \xref{valid/types}{valid-typeuse}{\vdash}

.. |vdashinstrtype| mathdef:: \xref{valid/types}{valid-instrtype}{\vdash}

.. |OKnumtype| mathdef:: \xref{valid/types}{valid-numtype}{\K{ok}}
.. |OKvectype| mathdef:: \xref{valid/types}{valid-vectype}{\K{ok}}
.. |OKheaptype| mathdef:: \xref{valid/types}{valid-heaptype}{\K{ok}}
.. |OKreftype| mathdef:: \xref{valid/types}{valid-reftype}{\K{ok}}
.. |OKvaltype| mathdef:: \xref{valid/types}{valid-valtype}{\K{ok}}
.. |OKresulttype| mathdef:: \xref{valid/types}{valid-resulttype}{\K{ok}}
.. |OKcomptype| mathdef:: \xref{valid/types}{valid-comptype}{\K{ok}}
.. |OKfieldtype| mathdef:: \xref{valid/types}{valid-fieldtype}{\K{ok}}
.. |OKpacktype| mathdef:: \xref{valid/types}{valid-packtype}{\K{ok}}
.. |OKstoragetype| mathdef:: \xref{valid/types}{valid-storagetype}{\K{ok}}
.. |OKsubtype| mathdef:: \xref{valid/types}{valid-subtype}{\K{ok}}
.. |OKsubtypeext| mathdef:: \xref{valid/types}{valid-subtype}{\K{ok}}
.. |OKrectype| mathdef:: \xref{valid/types}{valid-rectype}{\K{ok}}
.. |OKrectypeext| mathdef:: \xref{valid/types}{valid-rectype}{\K{ok}}
.. |OKdeftype| mathdef:: \xref{appendix/properties}{valid-deftype}{\K{ok}}
.. |OKtypeuse| mathdef:: \xref{valid/types}{valid-typeuse}{\K{ok}}
.. |OKtabletype| mathdef:: \xref{valid/types}{valid-tabletype}{\K{ok}}
.. |OKmemtype| mathdef:: \xref{valid/types}{valid-memtype}{\K{ok}}
.. |OKglobaltype| mathdef:: \xref{valid/types}{valid-globaltype}{\K{ok}}
.. |OKlocaltype| mathdef:: \xref{appendix/properties}{valid-localtype}{\K{ok}}
.. |OKtagtype| mathdef:: \xref{valid/types}{valid-tagtype}{\K{ok}}
.. |OKexterntype| mathdef:: \xref{valid/types}{valid-externtype}{\K{ok}}
.. |OKlimits| mathdef:: \xref{valid/types}{valid-limits}{\K{ok}}

.. |OKinstrtype| mathdef:: \xref{valid/types}{valid-instrtype}{\K{ok}}

.. |vdashnumtypematch| mathdef:: \xref{valid/matching}{match-numtype}{\vdash}
.. |vdashvectypematch| mathdef:: \xref{valid/matching}{match-vectype}{\vdash}
.. |vdashheaptypematch| mathdef:: \xref{valid/matching}{match-heaptype}{\vdash}
.. |vdashreftypematch| mathdef:: \xref{valid/matching}{match-reftype}{\vdash}
.. |vdashvaltypematch| mathdef:: \xref{valid/matching}{match-valtype}{\vdash}
.. |vdashresulttypematch| mathdef:: \xref{valid/matching}{match-resulttype}{\vdash}
.. |vdashinstrtypematch| mathdef:: \xref{valid/matching}{match-instrtype}{\vdash}
.. |vdashfieldtypematch| mathdef:: \xref{valid/matching}{match-fieldtype}{\vdash}
.. |vdashstoragetypematch| mathdef:: \xref{valid/matching}{match-storagetype}{\vdash}
.. |vdashpacktypematch| mathdef:: \xref{valid/matching}{match-packtype}{\vdash}
.. |vdashcomptypematch| mathdef:: \xref{valid/matching}{match-comptype}{\vdash}
.. |vdashdeftypematch| mathdef:: \xref{valid/matching}{match-deftype}{\vdash}
.. |vdashtabletypematch| mathdef:: \xref{valid/matching}{match-tabletype}{\vdash}
.. |vdashmemtypematch| mathdef:: \xref{valid/matching}{match-memtype}{\vdash}
.. |vdashglobaltypematch| mathdef:: \xref{valid/matching}{match-globaltype}{\vdash}
.. |vdashtagtypematch| mathdef:: \xref{valid/matching}{match-tagtype}{\vdash}
.. |vdashexterntypematch| mathdef:: \xref{valid/matching}{match-externtype}{\vdash}
.. |vdashlimitsmatch| mathdef:: \xref{valid/matching}{match-limits}{\vdash}

.. |subnumtypematch| mathdef:: \xref{valid/matching}{match-numtype}{\leq}
.. |subvectypematch| mathdef:: \xref{valid/matching}{match-vectype}{\leq}
.. |subheaptypematch| mathdef:: \xref{valid/matching}{match-heaptype}{\leq}
.. |subreftypematch| mathdef:: \xref{valid/matching}{match-reftype}{\leq}
.. |subvaltypematch| mathdef:: \xref{valid/matching}{match-valtype}{\leq}
.. |subresulttypematch| mathdef:: \xref{valid/matching}{match-resulttype}{\leq}
.. |subinstrtypematch| mathdef:: \xref{valid/matching}{match-instrtype}{\leq}
.. |subfieldtypematch| mathdef:: \xref{valid/matching}{match-fieldtype}{\leq}
.. |substoragetypematch| mathdef:: \xref{valid/matching}{match-storagetype}{\leq}
.. |subpacktypematch| mathdef:: \xref{valid/matching}{match-packtype}{\leq}
.. |subcomptypematch| mathdef:: \xref{valid/matching}{match-comptype}{\leq}
.. |subdeftypematch| mathdef:: \xref{valid/matching}{match-deftype}{\leq}
.. |subtabletypematch| mathdef:: \xref{valid/matching}{match-tabletype}{\leq}
.. |submemtypematch| mathdef:: \xref{valid/matching}{match-memtype}{\leq}
.. |subglobaltypematch| mathdef:: \xref{valid/matching}{match-globaltype}{\leq}
.. |subtagtypematch| mathdef:: \xref{valid/matching}{match-tagtype}{\leq}
.. |subexterntypematch| mathdef:: \xref{valid/matching}{match-externtype}{\leq}
.. |sublimitsmatch| mathdef:: \xref{valid/matching}{match-limits}{\leq}

.. |arrowmemarg| mathdef:: \xref{valid/instructions}{valid-memarg}{\rightarrow}
.. |vdashmemarg| mathdef:: \xref{valid/instructions}{valid-memarg}{\vdash}
.. |vdashinstr| mathdef:: \xref{valid/instructions}{valid-instr}{\vdash}
.. |vdashinstrs| mathdef:: \xref{valid/instructions}{valid-instrs}{\vdash}
.. |vdashcatch| mathdef:: \xref{valid/instructions}{valid-catch}{\vdash}
.. |vdashexpr| mathdef:: \xref{valid/instructions}{valid-expr}{\vdash}
.. |vdashinstrconst| mathdef:: \xref{valid/instructions}{valid-const}{\vdash}
.. |vdashexprconst| mathdef:: \xref{valid/instructions}{valid-const}{\vdash}
.. |vdashexprokconst| mathdef:: \xref{valid/instructions}{valid-const}{\vdash}

.. |OKcatch| mathdef:: \xref{valid/instructions}{valid-catch}{\K{ok}}

.. |CONSTinstrconst| mathdef:: \xref{valid/instructions}{valid-const}{\K{const}}
.. |CONSTexprconst| mathdef:: \xref{valid/instructions}{valid-const}{\K{const}}
.. |CONSTexprokconst| mathdef:: \xref{valid/instructions}{valid-const}{\K{const}}

.. |vdashexternidx| mathdef:: \xref{valid/modules}{valid-externidx}{\vdash}

.. |vdashtype| mathdef:: \xref{valid/modules}{valid-type}{\vdash}
.. |vdashtypes| mathdef:: \xref{valid/modules}{valid-types}{\vdash}
.. |vdashfunc| mathdef:: \xref{valid/modules}{valid-func}{\vdash}
.. |vdashlocal| mathdef:: \xref{valid/modules}{valid-local}{\vdash}
.. |vdashtable| mathdef:: \xref{valid/modules}{valid-table}{\vdash}
.. |vdashmem| mathdef:: \xref{valid/modules}{valid-mem}{\vdash}
.. |vdashglobal| mathdef:: \xref{valid/modules}{valid-global}{\vdash}
.. |vdashtag| mathdef:: \xref{valid/modules}{valid-tag}{\vdash}
.. |vdashglobals| mathdef:: \xref{valid/modules}{valid-globalseq}{\vdash}
.. |vdashelem| mathdef:: \xref{valid/modules}{valid-elem}{\vdash}
.. |vdashelemmode| mathdef:: \xref{valid/modules}{valid-elemmode}{\vdash}
.. |vdashdata| mathdef:: \xref{valid/modules}{valid-data}{\vdash}
.. |vdashdatamode| mathdef:: \xref{valid/modules}{valid-datamode}{\vdash}
.. |vdashstart| mathdef:: \xref{valid/modules}{valid-start}{\vdash}
.. |vdashexport| mathdef:: \xref{valid/modules}{valid-export}{\vdash}
.. |vdashimport| mathdef:: \xref{valid/modules}{valid-import}{\vdash}
.. |vdashmodule| mathdef:: \xref{valid/modules}{valid-module}{\vdash}

.. |OKelemmode| mathdef:: \xref{valid/modules}{valid-elemmode}{\K{ok}}
.. |OKdatamode| mathdef:: \xref{valid/modules}{valid-datamode}{\K{ok}}
.. |OKdata| mathdef:: \xref{valid/modules}{valid-data}{\K{ok}}
.. |OKstart| mathdef:: \xref{valid/modules}{valid-start}{\K{ok}}
.. |OKtypes| mathdef:: \xref{valid/modules}{valid-types}{\K{ok}}
.. |OKmodule| mathdef:: \xref{valid/modules}{valid-module}{\K{ok}}

.. |unpackshape| mathdef:: \xref{valid/instructions}{aux-unpackshape}{\F{unpack}}
.. |shlanetype| mathdef:: \xref{syntax/instructions}{aux-lanetype}{\F{lanetype}}
.. |shdim| mathdef:: \xref{syntax/instructions}{aux-dim}{\F{dim}}
.. |zeroop| mathdef:: \xref{syntax/instructions}{aux-zeroop}{\F{zeroop}}
.. |halfop| mathdef:: \xref{syntax/instructions}{aux-halfop}{\F{halfop}}

.. |vdashcontext| mathdef:: \xref{appendix/properties}{valid-context}{\vdash}
.. |OKcontext| mathdef:: \xref{appendix/properties}{valid-context}{\K{ok}}


.. Execution
.. ---------

.. Notation

.. |stepto| mathdef:: \xref{exec/conventions}{exec-notation}{\hookrightarrow}
.. |steptostar| mathdef:: \xref{exec/conventions}{exec-notation}{\hookrightarrow^\ast}
.. |extendsto| mathdef:: \xref{appendix/properties}{extend}{\preceq}


.. Allocation

.. |insttype| mathdef:: \xref{exec/types}{type-inst}{\F{clos}}

.. |alloctype| mathdef:: \xref{exec/modules}{alloc-type}{\F{alloctype}}
.. |allocfunc| mathdef:: \xref{exec/modules}{alloc-func}{\F{allocfunc}}
.. |alloctable| mathdef:: \xref{exec/modules}{alloc-table}{\F{alloctable}}
.. |allocmem| mathdef:: \xref{exec/modules}{alloc-mem}{\F{allocmem}}
.. |allocglobal| mathdef:: \xref{exec/modules}{alloc-global}{\F{allocglobal}}
.. |alloctag| mathdef:: \xref{exec/modules}{alloc-tag}{\F{alloctag}}
.. |allocelem| mathdef:: \xref{exec/modules}{alloc-elem}{\F{allocelem}}
.. |allocdata| mathdef:: \xref{exec/modules}{alloc-data}{\F{allocdata}}
.. |allocexport| mathdef:: \xref{exec/modules}{alloc-export}{\F{allocexport}}
.. |allocmodule| mathdef:: \xref{exec/modules}{alloc-module}{\F{allocmodule}}

.. |evalglobal| mathdef:: \xref{exec/modules}{eval-globals}{\F{evalglobal}}

.. |growtable| mathdef:: \xref{exec/modules}{grow-table}{\F{growtable}}
.. |growmem| mathdef:: \xref{exec/modules}{grow-mem}{\F{growmem}}

.. HACK !
.. |mm| mathdef:: \X{mm}


.. Addresses, non-terminals

.. |addr| mathdef:: \xref{exec/runtime}{syntax-addr}{\X{addr}}
.. |funcaddr| mathdef:: \xref{exec/runtime}{syntax-funcaddr}{\X{funcaddr}}
.. |tableaddr| mathdef:: \xref{exec/runtime}{syntax-tableaddr}{\X{tableaddr}}
.. |memaddr| mathdef:: \xref{exec/runtime}{syntax-memaddr}{\X{memaddr}}
.. |globaladdr| mathdef:: \xref{exec/runtime}{syntax-globaladdr}{\X{globaladdr}}
.. |tagaddr| mathdef:: \xref{exec/runtime}{syntax-tagaddr}{\X{tagaddr}}
.. |elemaddr| mathdef:: \xref{exec/runtime}{syntax-elemaddr}{\X{elemaddr}}
.. |dataaddr| mathdef:: \xref{exec/runtime}{syntax-dataaddr}{\X{dataaddr}}
.. |structaddr| mathdef:: \xref{exec/runtime}{syntax-structaddr}{\X{structaddr}}
.. |arrayaddr| mathdef:: \xref{exec/runtime}{syntax-arrayaddr}{\X{arrayaddr}}
.. |exnaddr| mathdef:: \xref{exec/runtime}{syntax-exnaddr}{\X{exnaddr}}
.. |hostaddr| mathdef:: \xref{exec/runtime}{syntax-hostaddr}{\X{hostaddr}}


.. Address, meta functions

.. |freefuncaddr| mathdef:: \xref{exec/runtime}{syntax-funcaddr}{\F{funcaddr}}
.. |freetableaddr| mathdef:: \xref{exec/runtime}{syntax-tableaddr}{\F{tableaddr}}
.. |freememaddr| mathdef:: \xref{exec/runtime}{syntax-memaddr}{\F{memaddr}}
.. |freeglobaladdr| mathdef:: \xref{exec/runtime}{syntax-globaladdr}{\F{globaladdr}}
.. |freetagaddr| mathdef:: \xref{exec/runtime}{syntax-globaladdr}{\F{tagaddr}}
.. |freeelemaddr| mathdef:: \xref{exec/runtime}{syntax-elemaddr}{\F{elemaddr}}
.. |freedataaddr| mathdef:: \xref{exec/runtime}{syntax-dataaddr}{\F{dataaddr}}


.. Instances, terminals

.. |FITYPE| mathdef:: \xref{exec/runtime}{syntax-funcinst}{\K{type}}
.. |FIMODULE| mathdef:: \xref{exec/runtime}{syntax-funcinst}{\K{module}}
.. |FICODE| mathdef:: \xref{exec/runtime}{syntax-funcinst}{\K{code}}
.. |FIHOSTFUNC| mathdef:: \xref{exec/runtime}{syntax-funcinst}{\K{hostfunc}}
.. |FIdots| mathdef:: \dots

.. |TITYPE| mathdef:: \xref{exec/runtime}{syntax-tableinst}{\K{type}}
.. |TIREFS| mathdef:: \xref{exec/runtime}{syntax-tableinst}{\K{refs}}

.. |MITYPE| mathdef:: \xref{exec/runtime}{syntax-meminst}{\K{type}}
.. |MIBYTES| mathdef:: \xref{exec/runtime}{syntax-meminst}{\K{bytes}}

.. |GITYPE| mathdef:: \xref{exec/runtime}{syntax-globalinst}{\K{type}}
.. |GIVALUE| mathdef:: \xref{exec/runtime}{syntax-globalinst}{\K{value}}

.. |HITYPE| mathdef:: \xref{exec/runtime}{syntax-taginst}{\K{type}}

.. |EITYPE| mathdef:: \xref{exec/runtime}{syntax-eleminst}{\K{type}}
.. |EIREFS| mathdef:: \xref{exec/runtime}{syntax-eleminst}{\K{refs}}

.. |DITYPE| mathdef:: \xref{exec/runtime}{syntax-datainst}{\K{data}}
.. |DIBYTES| mathdef:: \xref{exec/runtime}{syntax-datainst}{\K{bytes}}

.. |XINAME| mathdef:: \xref{exec/runtime}{syntax-exportinst}{\K{name}}
.. |XIADDR| mathdef:: \xref{exec/runtime}{syntax-exportinst}{\K{addr}}

.. |XAFUNC| mathdef:: \xref{exec/runtime}{syntax-externaddr}{\K{func}}
.. |XATABLE| mathdef:: \xref{exec/runtime}{syntax-externaddr}{\K{table}}
.. |XAMEM| mathdef:: \xref{exec/runtime}{syntax-externaddr}{\K{mem}}
.. |XAGLOBAL| mathdef:: \xref{exec/runtime}{syntax-externaddr}{\K{global}}
.. |XATAG| mathdef:: \xref{exec/runtime}{syntax-externaddr}{\K{tag}}

.. |MITYPES| mathdef:: \xref{exec/runtime}{syntax-moduleinst}{\K{types}}
.. |MIFUNCS| mathdef:: \xref{exec/runtime}{syntax-moduleinst}{\K{funcs}}
.. |MITABLES| mathdef:: \xref{exec/runtime}{syntax-moduleinst}{\K{tables}}
.. |MIMEMS| mathdef:: \xref{exec/runtime}{syntax-moduleinst}{\K{mems}}
.. |MIGLOBALS| mathdef:: \xref{exec/runtime}{syntax-moduleinst}{\K{globals}}
.. |MITAGS| mathdef:: \xref{exec/runtime}{syntax-moduleinst}{\K{tags}}
.. |MIELEMS| mathdef:: \xref{exec/runtime}{syntax-moduleinst}{\K{elems}}
.. |MIDATAS| mathdef:: \xref{exec/runtime}{syntax-moduleinst}{\K{datas}}
.. |MIEXPORTS| mathdef:: \xref{exec/runtime}{syntax-moduleinst}{\K{exports}}

.. |SITYPE| mathdef:: \xref{exec/runtime}{syntax-structinst}{\K{type}}
.. |SIFIELDS| mathdef:: \xref{exec/runtime}{syntax-structinst}{\K{fields}}

.. |AITYPE| mathdef:: \xref{exec/runtime}{syntax-arrayinst}{\K{type}}
.. |AIFIELDS| mathdef:: \xref{exec/runtime}{syntax-arrayinst}{\K{fields}}

.. |EITAG| mathdef:: \xref{exec/runtime}{syntax-exninst}{\K{tag}}
.. |EIFIELDS| mathdef:: \xref{exec/runtime}{syntax-exninst}{\K{fields}}

.. |PACK| mathdef:: \xref{exec/runtime}{syntax-packval}{\K{pack}}
.. |I8PACK| mathdef:: \xref{exec/runtime}{syntax-packval}{\K{i8.pack}}
.. |I16PACK| mathdef:: \xref{exec/runtime}{syntax-packval}{\K{i16.pack}}

.. |ZSTORE| mathdef:: \xref{exec/runtime}{syntax-state}{\K{store}}
.. |ZFRAME| mathdef:: \xref{exec/runtime}{syntax-state}{\K{frame}}
.. |ZMODULE| mathdef:: \xref{exec/runtime}{syntax-state}{\K{module}}
.. |ZTYPES| mathdef:: \xref{exec/runtime}{syntax-state}{\K{types}}
.. |ZFUNCS| mathdef:: \xref{exec/runtime}{syntax-state}{\K{funcs}}
.. |ZGLOBALS| mathdef:: \xref{exec/runtime}{syntax-state}{\K{globals}}
.. |ZTABLES| mathdef:: \xref{exec/runtime}{syntax-state}{\K{tables}}
.. |ZMEMS| mathdef:: \xref{exec/runtime}{syntax-state}{\K{mems}}
.. |ZTAGS| mathdef:: \xref{exec/runtime}{syntax-state}{\K{tags}}
.. |ZELEMS| mathdef:: \xref{exec/runtime}{syntax-state}{\K{elems}}
.. |ZDATAS| mathdef:: \xref{exec/runtime}{syntax-state}{\K{datas}}
.. |ZSTRUCTS| mathdef:: \xref{exec/runtime}{syntax-state}{\K{structs}}
.. |ZARRAYS| mathdef:: \xref{exec/runtime}{syntax-state}{\K{arrays}}
.. |ZEXNS| mathdef:: \xref{exec/runtime}{syntax-state}{\K{exns}}
.. |ZLOCALS| mathdef:: \xref{exec/runtime}{syntax-state}{\K{locals}}

.. |ZGGLOBALS| mathdef:: \ZGLOBALS
.. |ZGVALUE| mathdef:: \GIVALUE
.. |ZTTABLES| mathdef:: \ZTABLES
.. |ZTREFS| mathdef:: \TIREFS
.. |ZMMEMS| mathdef:: \ZMEMS
.. |ZMBYTES| mathdef:: \MIBYTES
.. |ZEELEMS| mathdef:: \ZELEMS
.. |ZEREFS| mathdef:: \EIREFS
.. |ZDDATAS| mathdef:: \ZDATAS
.. |ZDBYTES| mathdef:: \DIBYTES
.. |ZSSTRUCTS| mathdef:: \ZSTRUCTS
.. |ZSFIELDS| mathdef:: \SIFIELDS
.. |ZAARRAYS| mathdef:: \ZARRAYS
.. |ZAFIELDS| mathdef:: \AIFIELDS

.. Instances, non-terminals

.. |fieldval| mathdef:: \xref{exec/runtime}{syntax-fieldval}{\X{fieldval}}
.. |packval| mathdef:: \xref{exec/runtime}{syntax-packval}{\X{packval}}
.. |pack| mathdef:: \xref{exec/runtime}{syntax-pack}{\X{pack}}

.. |externaddr| mathdef:: \xref{exec/runtime}{syntax-externaddr}{\X{externaddr}}

.. |moduleinst| mathdef:: \xref{exec/runtime}{syntax-moduleinst}{\X{moduleinst}}
.. |funccode| mathdef:: \xref{exec/runtime}{syntax-funcinst}{\X{code}}
.. |funcinst| mathdef:: \xref{exec/runtime}{syntax-funcinst}{\X{funcinst}}
.. |tableinst| mathdef:: \xref{exec/runtime}{syntax-tableinst}{\X{tableinst}}
.. |meminst| mathdef:: \xref{exec/runtime}{syntax-meminst}{\X{meminst}}
.. |globalinst| mathdef:: \xref{exec/runtime}{syntax-globalinst}{\X{globalinst}}
.. |taginst| mathdef:: \xref{exec/runtime}{syntax-taginst}{\X{taginst}}
.. |eleminst| mathdef:: \xref{exec/runtime}{syntax-eleminst}{\X{eleminst}}
.. |datainst| mathdef:: \xref{exec/runtime}{syntax-datainst}{\X{datainst}}
.. |structinst| mathdef:: \xref{exec/runtime}{syntax-structinst}{\X{structinst}}
.. |arrayinst| mathdef:: \xref{exec/runtime}{syntax-arrayinst}{\X{arrayinst}}
.. |exportinst| mathdef:: \xref{exec/runtime}{syntax-exportinst}{\X{exportinst}}
.. |exninst| mathdef:: \xref{exec/runtime}{syntax-exninst}{\X{exninst}}

.. |hostfunc| mathdef:: \xref{exec/runtime}{syntax-hostfunc}{\X{hostfunc}}


.. Instances, meta functions

.. |funcsxa| mathdef:: \xref{exec/runtime}{syntax-externaddr}{\F{funcs}}
.. |tablesxa| mathdef:: \xref{exec/runtime}{syntax-externaddr}{\F{tables}}
.. |memsxa| mathdef:: \xref{exec/runtime}{syntax-externaddr}{\F{mems}}
.. |globalsxa| mathdef:: \xref{exec/runtime}{syntax-externaddr}{\F{globals}}
.. |tagsxa| mathdef:: \xref{exec/runtime}{syntax-externaddr}{\F{tags}}


.. Store, terminals

.. |SFUNCS| mathdef:: \xref{exec/runtime}{syntax-store}{\K{funcs}}
.. |STABLES| mathdef:: \xref{exec/runtime}{syntax-store}{\K{tables}}
.. |SMEMS| mathdef:: \xref{exec/runtime}{syntax-store}{\K{mems}}
.. |STAGS| mathdef:: \xref{exec/runtime}{syntax-store}{\K{tags}}
.. |SGLOBALS| mathdef:: \xref{exec/runtime}{syntax-store}{\K{globals}}
.. |SELEMS| mathdef:: \xref{exec/runtime}{syntax-store}{\K{elems}}
.. |SDATAS| mathdef:: \xref{exec/runtime}{syntax-store}{\K{datas}}
.. |SSTRUCTS| mathdef:: \xref{exec/runtime}{syntax-store}{\K{structs}}
.. |SARRAYS| mathdef:: \xref{exec/runtime}{syntax-store}{\K{arrays}}
.. |SEXNS| mathdef:: \xref{exec/runtime}{syntax-store}{\K{exns}}

.. Store, non-terminals

.. |store| mathdef:: \xref{exec/runtime}{syntax-store}{\X{store}}
.. |state| mathdef:: \xref{exec/runtime}{syntax-state}{\X{state}}


.. Stack, terminals

.. |LABEL| mathdef:: \xref{exec/runtime}{syntax-label}{\K{label}}
.. |FRAME| mathdef:: \xref{exec/runtime}{syntax-frame}{\K{frame}}
.. |HANDLER| mathdef:: \xref{exec/runtime}{syntax-handler}{\K{handler}}

.. |ALOCALS| mathdef:: \xref{exec/runtime}{syntax-frame}{\K{locals}}
.. |AMODULE| mathdef:: \xref{exec/runtime}{syntax-frame}{\K{module}}


.. Stack, non-terminals

.. |label| mathdef:: \xref{exec/runtime}{syntax-label}{\X{label}}
.. |handler| mathdef:: \xref{exec/runtime}{syntax-handler}{\X{handler}}
.. |frame| mathdef:: \xref{exec/runtime}{syntax-frame}{\X{frame}}
.. |callframe| mathdef:: \xref{exec/runtime}{syntax-callframe}{\X{callframe}}


.. Stack, meta functions

.. |fblocktype| mathdef:: \xref{exec/runtime}{aux-blocktype}{\F{instrtype}}


.. Administrative Instructions, terminals

.. |REFI31NUM| mathdef:: \xref{exec/runtime}{syntax-ref}{\K{ref{.}i\scriptstyle31}}
.. |REFNULLADDR| mathdef:: \xref{exec/runtime}{syntax-ref}{\K{ref{.}null}}
.. |REFFUNCADDR| mathdef:: \xref{exec/runtime}{syntax-ref}{\K{ref{.}func}}
.. |REFSTRUCTADDR| mathdef:: \xref{exec/runtime}{syntax-ref}{\K{ref{.}struct}}
.. |REFARRAYADDR| mathdef:: \xref{exec/runtime}{syntax-ref}{\K{ref{.}array}}
.. |REFEXNADDR| mathdef:: \xref{exec/runtime}{syntax-ref}{\K{ref{.}exn}}
.. |REFHOSTADDR| mathdef:: \xref{exec/runtime}{syntax-ref}{\K{ref{.}host}}
.. |REFEXTERN| mathdef:: \xref{exec/runtime}{syntax-ref}{\K{ref{.}extern}}
.. |TRAP| mathdef:: \xref{exec/runtime}{syntax-trap}{\K{trap}}


.. Values & Results, non-terminals

.. |num| mathdef:: \xref{exec/runtime}{syntax-num}{\X{num}}
.. |vec| mathdef:: \xref{exec/runtime}{syntax-vec}{\X{vec}}
.. |reff| mathdef:: \xref{exec/runtime}{syntax-ref}{\X{ref}}
.. |val| mathdef:: \xref{exec/runtime}{syntax-val}{\X{val}}
.. |result| mathdef:: \xref{exec/runtime}{syntax-result}{\X{result}}


.. Values, meta-functions

.. |default| mathdef:: \xref{exec/runtime}{aux-default}{\F{default}}

.. |packnum| mathdef:: \xref{exec/numerics}{aux-packnum}{\F{pack}}
.. |unpacknum| mathdef:: \xref{exec/numerics}{aux-unpacknum}{\F{unpack}}


.. Fields, meta-functions

.. |packfield| mathdef:: \xref{exec/runtime}{aux-packfield}{\F{pack}}
.. |unpackfield| mathdef:: \xref{exec/runtime}{aux-unpackfield}{\F{unpack}}


.. Configurations, non-terminals

.. |config| mathdef:: \xref{exec/runtime}{syntax-config}{\X{config}}
.. |thread| mathdef:: \xref{exec/runtime}{syntax-thread}{\X{thread}}


.. Numerics, operators

.. |iadd| mathdef:: \xref{exec/numerics}{op-iadd}{\F{iadd}}
.. |isub| mathdef:: \xref{exec/numerics}{op-isub}{\F{isub}}
.. |imul| mathdef:: \xref{exec/numerics}{op-imul}{\F{imul}}
.. |idiv| mathdef:: \xref{exec/numerics}{op-idiv}{\F{idiv}}
.. |idivu| mathdef:: \xref{exec/numerics}{op-idiv}{\F{idiv\_u}}
.. |idivs| mathdef:: \xref{exec/numerics}{op-idiv}{\F{idiv\_s}}
.. |irem| mathdef:: \xref{exec/numerics}{op-irem}{\F{irem}}
.. |iremu| mathdef:: \xref{exec/numerics}{op-irem}{\F{irem\_u}}
.. |irems| mathdef:: \xref{exec/numerics}{op-irem}{\F{irem\_s}}
.. |inot| mathdef:: \xref{exec/numerics}{op-inot}{\F{inot}}
.. |irev| mathdef:: \xref{exec/numerics}{op-irev}{\F{irev}}
.. |iand| mathdef:: \xref{exec/numerics}{op-iand}{\F{iand}}
.. |iandnot| mathdef:: \xref{exec/numerics}{op-iandnot}{\F{iandnot}}
.. |ior| mathdef:: \xref{exec/numerics}{op-ior}{\F{ior}}
.. |ixor| mathdef:: \xref{exec/numerics}{op-ixor}{\F{ixor}}
.. |ishl| mathdef:: \xref{exec/numerics}{op-ishl}{\F{ishl}}
.. |ishr| mathdef:: \xref{exec/numerics}{op-ishr}{\F{ishr}}
.. |ishru| mathdef:: \xref{exec/numerics}{op-ishr}{\F{ishr\_u}}
.. |ishrs| mathdef:: \xref{exec/numerics}{op-ishr}{\F{ishr\_s}}
.. |irotl| mathdef:: \xref{exec/numerics}{op-irotl}{\F{irotl}}
.. |irotr| mathdef:: \xref{exec/numerics}{op-irotr}{\F{irotr}}
.. |iclz| mathdef:: \xref{exec/numerics}{op-iclz}{\F{iclz}}
.. |ictz| mathdef:: \xref{exec/numerics}{op-ictz}{\F{ictz}}
.. |ipopcnt| mathdef:: \xref{exec/numerics}{op-ipopcnt}{\F{ipopcnt}}
.. |ieqz| mathdef:: \xref{exec/numerics}{op-ieqz}{\F{ieqz}}
.. |inez| mathdef:: \xref{exec/numerics}{op-inez}{\F{inez}}
.. |ieq| mathdef:: \xref{exec/numerics}{op-ieq}{\F{ieq}}
.. |ine| mathdef:: \xref{exec/numerics}{op-ine}{\F{ine}}
.. |ilt| mathdef:: \xref{exec/numerics}{op-ilt}{\F{ilt}}
.. |iltu| mathdef:: \xref{exec/numerics}{op-ilt}{\F{ilt\_u}}
.. |ilts| mathdef:: \xref{exec/numerics}{op-ilt}{\F{ilt\_s}}
.. |igt| mathdef:: \xref{exec/numerics}{op-igt}{\F{igt}}
.. |igtu| mathdef:: \xref{exec/numerics}{op-igt}{\F{igt\_u}}
.. |igts| mathdef:: \xref{exec/numerics}{op-igt}{\F{igt\_s}}
.. |ile| mathdef:: \xref{exec/numerics}{op-ile}{\F{ile}}
.. |ileu| mathdef:: \xref{exec/numerics}{op-ile}{\F{ile\_u}}
.. |iles| mathdef:: \xref{exec/numerics}{op-ile}{\F{ile\_s}}
.. |ige| mathdef:: \xref{exec/numerics}{op-ige}{\F{ige}}
.. |igeu| mathdef:: \xref{exec/numerics}{op-ige}{\F{ige\_u}}
.. |iges| mathdef:: \xref{exec/numerics}{op-ige}{\F{ige\_s}}
.. |iextendMs| mathdef:: \xref{exec/numerics}{op-iextendn}{\F{iextend}M\F{\_s}}
.. |ibitselect| mathdef:: \xref{exec/numerics}{op-ibitselect}{\F{ibitselect}}
.. |iabs| mathdef:: \xref{exec/numerics}{op-iabs}{\F{iabs}}
.. |ineg| mathdef:: \xref{exec/numerics}{op-ineg}{\F{ineg}}
.. |imin| mathdef:: \xref{exec/numerics}{op-imin}{\F{imin}}
.. |iminu| mathdef:: \xref{exec/numerics}{op-imin}{\F{imin\_u}}
.. |imins| mathdef:: \xref{exec/numerics}{op-imin}{\F{imin\_s}}
.. |imax| mathdef:: \xref{exec/numerics}{op-imax}{\F{imax}}
.. |imaxu| mathdef:: \xref{exec/numerics}{op-imax}{\F{imax\_u}}
.. |imaxs| mathdef:: \xref{exec/numerics}{op-imax}{\F{imax\_s}}
.. |iaddsat| mathdef:: \xref{exec/numerics}{op-iadd_sat}{\F{iadd\_sat}}
.. |iaddsatu| mathdef:: \xref{exec/numerics}{op-iadd_sat}{\F{iadd\_sat\_u}}
.. |iaddsats| mathdef:: \xref{exec/numerics}{op-iadd_sat}{\F{iadd\_sat\_s}}
.. |isubsat| mathdef:: \xref{exec/numerics}{op-isub_sat}{\F{isub\_sat}}
.. |isubsatu| mathdef:: \xref{exec/numerics}{op-isub_sat}{\F{isub\_sat\_u}}
.. |isubsats| mathdef:: \xref{exec/numerics}{op-isub_sat}{\F{isub\_sat\_s}}
.. |iavgr| mathdef:: \xref{exec/numerics}{op-iavgr}{\F{iavgr}}
.. |iavgru| mathdef:: \xref{exec/numerics}{op-iavgr}{\F{iavgr\_u}}
.. |iq15mulrsat| mathdef:: \xref{exec/numerics}{op-iq15mulrsat}{\F{iq15mulrsat}}
.. |iq15mulrsats| mathdef:: \xref{exec/numerics}{op-iq15mulrsat}{\F{iq15mulrsat\_s}}

.. |fadd| mathdef:: \xref{exec/numerics}{op-fadd}{\F{fadd}}
.. |fsub| mathdef:: \xref{exec/numerics}{op-fsub}{\F{fsub}}
.. |fmul| mathdef:: \xref{exec/numerics}{op-fmul}{\F{fmul}}
.. |fdiv| mathdef:: \xref{exec/numerics}{op-fdiv}{\F{fdiv}}
.. |fma| mathdef:: \xref{exec/numerics}{op-fma}{\F{fma}}
.. |fmin| mathdef:: \xref{exec/numerics}{op-fmin}{\F{fmin}}
.. |fmax| mathdef:: \xref{exec/numerics}{op-fmax}{\F{fmax}}
.. |fcopysign| mathdef:: \xref{exec/numerics}{op-fcopysign}{\F{fcopysign}}
.. |fabs| mathdef:: \xref{exec/numerics}{op-fabs}{\F{fabs}}
.. |fneg| mathdef:: \xref{exec/numerics}{op-fneg}{\F{fneg}}
.. |fsqrt| mathdef:: \xref{exec/numerics}{op-fsqrt}{\F{fsqrt}}
.. |fceil| mathdef:: \xref{exec/numerics}{op-fceil}{\F{fceil}}
.. |ffloor| mathdef:: \xref{exec/numerics}{op-ffloor}{\F{ffloor}}
.. |ftrunc| mathdef:: \xref{exec/numerics}{op-ftrunc}{\F{ftrunc}}
.. |fnearest| mathdef:: \xref{exec/numerics}{op-fnearest}{\F{fnearest}}
.. |feq| mathdef:: \xref{exec/numerics}{op-feq}{\F{feq}}
.. |fne| mathdef:: \xref{exec/numerics}{op-fne}{\F{fne}}
.. |flt| mathdef:: \xref{exec/numerics}{op-flt}{\F{flt}}
.. |fgt| mathdef:: \xref{exec/numerics}{op-fgt}{\F{fgt}}
.. |fle| mathdef:: \xref{exec/numerics}{op-fle}{\F{fle}}
.. |fge| mathdef:: \xref{exec/numerics}{op-fge}{\F{fge}}
.. |fpmin| mathdef:: \xref{exec/numerics}{op-fpmin}{\F{fpmin}}
.. |fpmax| mathdef:: \xref{exec/numerics}{op-fpmax}{\F{fpmax}}

.. |extend| mathdef:: \xref{exec/numerics}{op-extend}{\F{extend}}
.. |extendu| mathdef:: \xref{exec/numerics}{op-extend}{\F{extend}^{\K{u}}}
.. |extends| mathdef:: \xref{exec/numerics}{op-extend}{\F{extend}^{\K{s}}}
.. |wrap| mathdef:: \xref{exec/numerics}{op-wrap}{\F{wrap}}
.. |trunc| mathdef:: \xref{exec/numerics}{op-trunc}{\F{trunc}}
.. |truncu| mathdef:: \xref{exec/numerics}{op-trunc}{\F{trunc}^{\K{u}}}
.. |truncs| mathdef:: \xref{exec/numerics}{op-trunc}{\F{trunc}^{\K{s}}}
.. |truncsat| mathdef:: \xref{exec/numerics}{op-trunc_sat}{\F{trunc\_sat}}
.. |truncsatu| mathdef:: \xref{exec/numerics}{op-trunc_sat}{\F{trunc\_sat\_u}}
.. |truncsats| mathdef:: \xref{exec/numerics}{op-trunc_sat}{\F{trunc\_sat\_s}}
.. |promote| mathdef:: \xref{exec/numerics}{op-promote}{\F{promote}}
.. |demote| mathdef:: \xref{exec/numerics}{op-demote}{\F{demote}}
.. |convert| mathdef:: \xref{exec/numerics}{op-convert}{\F{convert}}
.. |convertu| mathdef:: \xref{exec/numerics}{op-convert}{\F{convert}^{\K{u}}}
.. |converts| mathdef:: \xref{exec/numerics}{op-convert}{\F{convert}^{\K{s}}}
.. |reinterpret| mathdef:: \xref{exec/numerics}{op-reinterpret}{\F{reinterpret}}
.. |narrow| mathdef:: \xref{exec/numerics}{op-narrow}{\F{narrow}}
.. |narrowu| mathdef:: \xref{exec/numerics}{op-narrow}{\F{narrow}^{\K{u}}}
.. |narrows| mathdef:: \xref{exec/numerics}{op-narrow}{\F{narrow}^{\K{s}}}

.. |ivbitmask| mathdef:: \xref{exec/numerics}{op-ivbitmask}{\F{ivbitmask}}
.. |ivswizzlelane| mathdef:: \xref{exec/numerics}{op-ivswizzle_lane}{\F{ivswizzle\_lane}}
.. |ivswizzle| mathdef:: \xref{exec/numerics}{op-ivswizzle}{\F{ivswizzle}}
.. |ivshuffle| mathdef:: \xref{exec/numerics}{op-ivshuffle}{\F{ivshuffle}}
.. |ivaddpairwise| mathdef:: \xref{exec/numerics}{op-ivadd_pairwise}{\F{ivadd\_pairwise}}
.. |ivmul| mathdef:: \xref{exec/numerics}{op-ivmul}{\F{ivmul}}
.. |ivdot| mathdef:: \xref{exec/numerics}{op-ivdot}{\F{ivdot}}
.. |ivdotsat| mathdef:: \xref{exec/numerics}{op-ivdot_sat}{\F{ivdotsat}}

.. |frelaxedmadd| mathdef:: \xref{exec/numerics}{op-frelaxed_madd}{\F{frelaxed\_madd}}
.. |frelaxednmadd| mathdef:: \xref{exec/numerics}{op-frelaxed_nmadd}{\F{frelaxed\_nmadd}}
.. |ivrelaxedswizzlelane| mathdef:: \xref{exec/numerics}{op-ivrelaxed_swizzle_lane}{\F{ivrelaxed\_swizzle\_lane}}
.. |ivrelaxedswizzle| mathdef:: \xref{exec/numerics}{op-ivrelaxed_swizzle}{\F{ivrelaxed\_swizzle}}
.. |relaxedtrunc| mathdef:: \xref{exec/numerics}{op-relaxed_trunc}{\F{relaxed\_trunc}}
.. |irelaxedlaneselect| mathdef:: \xref{exec/numerics}{op-irelaxed_laneselect}{\F{irelaxed\_laneselect}}
.. |frelaxedmin| mathdef:: \xref{exec/numerics}{op-frelaxed_min}{\F{frelaxed\_min}}
.. |frelaxedmax| mathdef:: \xref{exec/numerics}{op-frelaxed_max}{\F{frelaxed\_max}}
.. |irelaxedq15mulrs| mathdef:: \xref{exec/numerics}{op-irelaxed_q15mulr_s}{\F{irelaxed\_q15mulr\_s}}
.. |irelaxeddot| mathdef:: \xref{exec/numerics}{op-irelaxed_dot}{\F{irelaxed\_dot}}


.. Numerics, meta functions

.. |bits| mathdef:: \xref{exec/numerics}{aux-bits}{\F{bits}}
.. |ibits| mathdef:: \xref{exec/numerics}{aux-ibits}{\F{ibits}}
.. |fbits| mathdef:: \xref{exec/numerics}{aux-fbits}{\F{fbits}}
.. |fsign| mathdef:: \xref{exec/numerics}{aux-fsign}{\F{fsign}}
.. |fbias| mathdef:: \xref{exec/numerics}{aux-fbias}{\F{fbias}}
.. |bytes| mathdef:: \xref{exec/numerics}{aux-bytes}{\F{bytes}}
.. |littleendian| mathdef:: \xref{exec/numerics}{aux-littleendian}{\F{littleendian}}
.. |signed| mathdef:: \xref{exec/numerics}{aux-signed}{\F{signed}}
.. |tobool| mathdef:: \xref{exec/numerics}{aux-tobool}{\F{bool}}

.. |ieee| mathdef:: \xref{exec/numerics}{aux-ieee}{\F{float}}
.. |nans| mathdef:: \xref{exec/numerics}{aux-nans}{\F{nans}}
.. |truncz| mathdef:: \xref{exec/numerics}{aux-trunc}{\F{trunc}}
.. |sat| mathdef:: \xref{exec/numerics}{aux-sat}{\F{sat}}
.. |satu| mathdef:: \xref{exec/numerics}{aux-sat}{\F{sat\_u}}
.. |sats| mathdef:: \xref{exec/numerics}{aux-sat}{\F{sat\_s}}

.. |lanes| mathdef:: \xref{exec/numerics}{aux-lanes}{\F{lanes}}

.. |relaxed| mathdef:: \xref{exec/numerics}{aux-relaxed}{\F{relaxed}}


.. Other meta functions

.. |instantiate| mathdef:: \xref{exec/modules}{exec-instantiation}{\F{instantiate}}
.. |invoke| mathdef:: \xref{exec/modules}{exec-invocation}{\F{invoke}}

.. |runelem| mathdef:: \xref{exec/modules}{aux-runelem}{\F{runelem}}
.. |rundata| mathdef:: \xref{exec/modules}{aux-rundata}{\F{rundata}}


.. Judgements

.. |vdashnum| mathdef:: \xref{exec/values}{valid-num}{\vdash}
.. |vdashvec| mathdef:: \xref{exec/values}{valid-vec}{\vdash}
.. |vdashref| mathdef:: \xref{exec/values}{valid-ref}{\vdash}
.. |vdashval| mathdef:: \xref{exec/values}{valid-val}{\vdash}
.. |vdashexternaddr| mathdef:: \xref{exec/values}{valid-externaddr}{\vdash}


.. Soundness
.. ---------

.. Judgements

.. |vdashadmininstr| mathdef:: \xref{appendix/properties}{valid-instr-admin}{\vdash}

.. |vdashresult| mathdef:: \xref{appendix/properties}{valid-result}{\vdash}
.. |vdashfieldval| mathdef:: \xref{appendix/properties}{valid-fieldval}{\vdash}
.. |vdashpackval| mathdef:: \xref{appendix/properties}{valid-packval}{\vdash}

.. |vdashfuncinst| mathdef:: \xref{appendix/properties}{valid-funcinst}{\vdash}
.. |vdashtableinst| mathdef:: \xref{appendix/properties}{valid-tableinst}{\vdash}
.. |vdashmeminst| mathdef:: \xref{appendix/properties}{valid-meminst}{\vdash}
.. |vdashglobalinst| mathdef:: \xref{appendix/properties}{valid-globalinst}{\vdash}
.. |vdashtaginst| mathdef:: \xref{appendix/properties}{valid-taginst}{\vdash}
.. |vdasheleminst| mathdef:: \xref{appendix/properties}{valid-eleminst}{\vdash}
.. |vdashdatainst| mathdef:: \xref{appendix/properties}{valid-datainst}{\vdash}
.. |vdashstructinst| mathdef:: \xref{appendix/properties}{valid-structinst}{\vdash}
.. |vdasharrayinst| mathdef:: \xref{appendix/properties}{valid-arrayinst}{\vdash}
.. |vdashexninst| mathdef:: \xref{appendix/properties}{valid-exninst}{\vdash}
.. |vdashexportinst| mathdef:: \xref{appendix/properties}{valid-exportinst}{\vdash}
.. |vdashmoduleinst| mathdef:: \xref{appendix/properties}{valid-moduleinst}{\vdash}

.. |OKtaginst| mathdef:: \xref{appendix/properties}{valid-taginst}{\K{ok}}
.. |OKdatainst| mathdef:: \xref{appendix/properties}{valid-datainst}{\K{ok}}
.. |OKstructinst| mathdef:: \xref{appendix/properties}{valid-structinst}{\K{ok}}
.. |OKarrayinst| mathdef:: \xref{appendix/properties}{valid-arrayinst}{\K{ok}}
.. |OKexninst| mathdef:: \xref{appendix/properties}{valid-exninst}{\K{ok}}
.. |OKexportinst| mathdef:: \xref{appendix/properties}{valid-exportinst}{\K{ok}}

.. |vdashcontext| mathdef:: \xref{appendix/properties}{valid-context}{\vdash}
.. |vdashstore| mathdef:: \xref{appendix/properties}{valid-store}{\vdash}
.. |vdashconfig| mathdef:: \xref{appendix/properties}{valid-config}{\vdash}
.. |vdashthread| mathdef:: \xref{appendix/properties}{valid-thread}{\vdash}
.. |vdashframe| mathdef:: \xref{appendix/properties}{valid-frame}{\vdash}

.. |OKstore| mathdef:: \xref{appendix/properties}{valid-store}{\K{ok}}

.. |vdashfuncinstextends| mathdef:: \xref{appendix/properties}{extend-funcinst}{\vdash}
.. |vdashtableinstextends| mathdef:: \xref{appendix/properties}{extend-tableinst}{\vdash}
.. |vdashmeminstextends| mathdef:: \xref{appendix/properties}{extend-meminst}{\vdash}
.. |vdashglobalinstextends| mathdef:: \xref{appendix/properties}{extend-globalinst}{\vdash}
.. |vdashtaginstextends| mathdef:: \xref{appendix/properties}{extend-taginst}{\vdash}
.. |vdasheleminstextends| mathdef:: \xref{appendix/properties}{extend-eleminst}{\vdash}
.. |vdashdatainstextends| mathdef:: \xref{appendix/properties}{extend-datainst}{\vdash}
.. |vdashstructinstextends| mathdef:: \xref{appendix/properties}{extend-structinst}{\vdash}
.. |vdasharrayinstextends| mathdef:: \xref{appendix/properties}{extend-arrayinst}{\vdash}
.. |vdashexninstextends| mathdef:: \xref{appendix/properties}{extend-exninst}{\vdash}
.. |vdashstoreextends| mathdef:: \xref{appendix/properties}{extend-store}{\vdash}


.. Custom Sections
.. ---------------

.. Name section, non-terminals

.. |Bnamesec| mathdef:: \xref{appendix/custom}{binary-namesubsection}{\B{namesec}}
.. |Bnamedata| mathdef:: \xref{appendix/custom}{binary-namesubsection}{\B{namedata}}
.. |Bnamesubsection| mathdef:: \xref{appendix/custom}{binary-namesubsection}{\B{namesubsection}}

.. |Bnamemap| mathdef:: \xref{appendix/custom}{binary-namemap}{\B{namemap}}
.. |Bnameassoc| mathdef:: \xref{appendix/custom}{binary-namemap}{\B{nameassoc}}
.. |Bindirectnamemap| mathdef:: \xref{appendix/custom}{binary-indirectnamemap}{\B{indirectnamemap}}
.. |Bindirectnameassoc| mathdef:: \xref{appendix/custom}{binary-indirectnamemap}{\B{indirectnameassoc}}

.. |Bmodulenamesubsec| mathdef:: \xref{appendix/custom}{binary-modulenamesec}{\B{modulenamesubsec}}
.. |Bfuncnamesubsec| mathdef:: \xref{appendix/custom}{binary-funcnamesec}{\B{funcnamesubsec}}
.. |Btagnamesubsec| mathdef:: \xref{appendix/custom}{binary-tagnamesec}{\B{tagnamesubsec}}
.. |Blocalnamesubsec| mathdef:: \xref{appendix/custom}{binary-localnamesec}{\B{localnamesubsec}}
.. |Btypenamesubsec| mathdef:: \xref{appendix/custom}{binary-typenamesec}{\B{typenamesubsec}}
.. |Bfieldnamesubsec| mathdef:: \xref{appendix/custom}{binary-fieldnamesec}{\B{fieldnamesubsec}}


.. Annotations
.. -----------

.. Custom annotations, non-terminals

.. |Tcustomannot| mathdef:: \xref{appendix/custom}{text-customannot}{\T{customannot}}
.. |Tcustomplace| mathdef:: \xref{appendix/custom}{text-customannot}{\T{customplace}}
.. |Tsec| mathdef:: \xref{appendix/custom}{text-customannot}{\T{sec}}


.. Name annotations, non-terminals

.. |Tnameannot| mathdef:: \xref{appendix/custom}{text-nameannot}{\T{nameannot}}
.. |Tmodulenameannot| mathdef:: \xref{appendix/custom}{text-modulenameannot}{\T{modulenameannot}}
.. |Tfuncnameannot| mathdef:: \xref{appendix/custom}{text-funcnameannot}{\T{funcnameannot}}
.. |Tparamnameannot| mathdef:: \xref{appendix/custom}{text-paramnameannot}{\T{paramnameannot}}
.. |Tlocalnameannot| mathdef:: \xref{appendix/custom}{text-localnameannot}{\T{localnameannot}}
.. |Ttypenameannot| mathdef:: \xref{appendix/custom}{text-typenameannot}{\T{typenameannot}}
.. |Tfieldnameannot| mathdef:: \xref{appendix/custom}{text-fieldnameannot}{\T{fieldnameannot}}
.. |Ttagnameannot| mathdef:: \xref{appendix/custom}{text-tagnameannot}{\T{tagnameannot}}


.. Embedding
.. ---------

.. |bool| mathdef:: \xref{appendix/embedding}{embed-bool}{\X{bool}}
.. |TRUE| mathdef:: \xref{appendix/embedding}{embed-bool}{\X{true}}
.. |FALSE| mathdef:: \xref{appendix/embedding}{embed-bool}{\X{false}}

.. |error| mathdef:: \xref{appendix/embedding}{embed-error}{\X{error}}
.. |ERROR| mathdef:: \xref{appendix/embedding}{embed-error}{\K{error}}
.. |exception| mathdef:: \xref{appendix/embedding}{embed-error}{\X{exception}}
.. |EXCEPTION| mathdef:: \xref{appendix/embedding}{embed-error}{\K{exception}}