Types
Simple types, such as number types are universally valid.
However, restrictions apply to most other types, such as reference types, function types, as well as the limits of table types and memory types, which must be checked during validation.
Moreover, block types are converted to plain function types for ease of processing.
Number Types
Number types are always valid.
\[\begin{array}{@{}c@{}}\displaystyle
\frac{
}{
C \href{../valid/types.html#valid-numtype}{\vdash} {\href{../syntax/types.html#syntax-numtype}{\mathit{numtype}}} : \href{../valid/types.html#valid-numtype}{\mathsf{ok}}
}
\qquad
\end{array}\]
Vector Types
Vector types are always valid.
\[\begin{array}{@{}c@{}}\displaystyle
\frac{
}{
C \href{../valid/types.html#valid-vectype}{\vdash} {\href{../syntax/types.html#syntax-vectype}{\mathit{vectype}}} : \href{../valid/types.html#valid-vectype}{\mathsf{ok}}
}
\qquad
\end{array}\]
Heap Types
Concrete heap types are only valid when the type index is,
while abstract ones are vacuously valid.
\(\href{../syntax/types.html#syntax-absheaptype}{\mathit{absheaptype}}\)
\[\begin{array}{@{}c@{}}\displaystyle
\frac{
}{
C \href{../valid/types.html#valid-heaptype}{\vdash} {\href{../syntax/types.html#syntax-absheaptype}{\mathit{absheaptype}}} : \href{../valid/types.html#valid-heaptype}{\mathsf{ok}}
}
\qquad
\end{array}\]
\(\href{../syntax/modules.html#syntax-typeidx}{\mathit{typeidx}}\)
\[\begin{array}{@{}c@{}}\displaystyle
\frac{
C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[{\href{../syntax/modules.html#syntax-typeidx}{\mathit{typeidx}}}] = {\mathit{dt}}
}{
C \href{../valid/types.html#valid-heaptype}{\vdash} {\href{../syntax/modules.html#syntax-typeidx}{\mathit{typeidx}}} : \href{../valid/types.html#valid-heaptype}{\mathsf{ok}}
}
\qquad
\end{array}\]
Reference Types
Reference types are valid when the referenced heap type is.
\(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}^?~\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}\)
\[\begin{array}{@{}c@{}}\displaystyle
\frac{
C \href{../valid/types.html#valid-heaptype}{\vdash} {\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}} : \href{../valid/types.html#valid-heaptype}{\mathsf{ok}}
}{
C \href{../valid/types.html#valid-reftype}{\vdash} \href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~{\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}^?}~{\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}} : \href{../valid/types.html#valid-reftype}{\mathsf{ok}}
}
\qquad
\end{array}\]
Block Types
Block types may be expressed in one of two forms, both of which are converted to instruction types by the following rules.
\(\href{../syntax/modules.html#syntax-typeidx}{\mathit{typeidx}}\)
The type \(C.\href{../valid/conventions.html#context}{\mathsf{types}}[\href{../syntax/modules.html#syntax-typeidx}{\mathit{typeidx}}]\) must be defined in the context.
The expansion of \(C.\href{../valid/conventions.html#context}{\mathsf{funcs}}[\href{../syntax/modules.html#syntax-typeidx}{\mathit{typeidx}}]\) must be a function type \(\href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~[t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast]\).
Then the block type is valid as instruction type \([t_1^\ast] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [t_2^\ast]\).
\[\begin{array}{@{}c@{}}\displaystyle
\frac{
C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[{\href{../syntax/modules.html#syntax-typeidx}{\mathit{typeidx}}}] \href{../valid/conventions.html#aux-expand-deftype}{\approx} \href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~({t_1^\ast} \href{../syntax/types.html#syntax-functype}{\rightarrow} {t_2^\ast})
}{
C \href{../valid/types.html#valid-blocktype}{\vdash} {\href{../syntax/modules.html#syntax-typeidx}{\mathit{typeidx}}} : {t_1^\ast} \rightarrow {t_2^\ast}
}
\qquad
\end{array}\]
\([\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}^?]\)
The value type \(\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}\) must either be absent, or valid.
Then the block type is valid as instruction type \([] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}^?]\).
\[\begin{array}{@{}c@{}}\displaystyle
\frac{
(C \href{../valid/types.html#valid-valtype}{\vdash} {\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}} : \href{../valid/types.html#valid-valtype}{\mathsf{ok}})^?
}{
C \href{../valid/types.html#valid-blocktype}{\vdash} {{\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}}^?} : \epsilon \rightarrow {{\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}}^?}
}
\qquad
\end{array}\]
Result Types
\([t^\ast]\)
\[\begin{array}{@{}c@{}}\displaystyle
\frac{
(C \href{../valid/types.html#valid-valtype}{\vdash} t : \href{../valid/types.html#valid-valtype}{\mathsf{ok}})^\ast
}{
C \href{../valid/types.html#valid-resulttype}{\vdash} {t^\ast} : \href{../valid/types.html#valid-resulttype}{\mathsf{ok}}
}
\qquad
\end{array}\]
Instruction Types
\([t_1^\ast] \rightarrow_{x^\ast} [t_2^\ast]\)
\[\begin{array}{@{}c@{}}\displaystyle
\frac{
C \href{../valid/types.html#valid-resulttype}{\vdash} {t_1^\ast} : \href{../valid/types.html#valid-resulttype}{\mathsf{ok}}
\qquad
C \href{../valid/types.html#valid-resulttype}{\vdash} {t_2^\ast} : \href{../valid/types.html#valid-resulttype}{\mathsf{ok}}
\qquad
(C{.}\href{../valid/conventions.html#context}{\mathsf{locals}}{}[x] = {{\mathit{lt}}})^\ast
}{
C \href{../valid/types.html#valid-instrtype}{\vdash} {t_1^\ast} \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}_{{x^\ast}} {t_2^\ast} : \href{../valid/types.html#valid-instrtype}{\mathsf{ok}}
}
\qquad
\end{array}\]
Function Types
\([t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast]\)
\[\begin{array}{@{}c@{}}\displaystyle
\frac{
C \href{../valid/types.html#valid-resulttype}{\vdash} {t_1^\ast} : \href{../valid/types.html#valid-resulttype}{\mathsf{ok}}
\qquad
C \href{../valid/types.html#valid-resulttype}{\vdash} {t_2^\ast} : \href{../valid/types.html#valid-resulttype}{\mathsf{ok}}
}{
C \href{../valid/types.html#valid-functype}{\vdash} {t_1^\ast} \href{../syntax/types.html#syntax-functype}{\rightarrow} {t_2^\ast} : \href{../valid/types.html#valid-functype}{\mathsf{ok}}
}
\qquad
\end{array}\]
Composite Types
\(\href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~\href{../syntax/types.html#syntax-functype}{\mathit{functype}}\)
\[\begin{array}{@{}c@{}}\displaystyle
\frac{
C \href{../valid/types.html#valid-functype}{\vdash} {\href{../syntax/types.html#syntax-functype}{\mathit{functype}}} : \href{../valid/types.html#valid-functype}{\mathsf{ok}}
}{
C \href{../valid/types.html#valid-comptype}{\vdash} \href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~{\href{../syntax/types.html#syntax-functype}{\mathit{functype}}} : \href{../valid/types.html#valid-comptype}{\mathsf{ok}}
}
\qquad
\end{array}\]
\(\href{../syntax/types.html#syntax-comptype}{\mathsf{struct}}~\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}^\ast\)
For each field type \(\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}_i\) in \(\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}^\ast\):
Then the composite type is valid.
\[\begin{array}{@{}c@{}}\displaystyle
\frac{
(C \href{../valid/types.html#valid-fieldtype}{\vdash} {\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}} : \href{../valid/types.html#valid-fieldtype}{\mathsf{ok}})^\ast
}{
C \href{../valid/types.html#valid-comptype}{\vdash} \href{../syntax/types.html#syntax-comptype}{\mathsf{struct}}~{{\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}}^\ast} : \href{../valid/types.html#valid-comptype}{\mathsf{ok}}
}
\qquad
\end{array}\]
\(\href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}\)
\[\begin{array}{@{}c@{}}\displaystyle
\frac{
C \href{../valid/types.html#valid-fieldtype}{\vdash} {\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}} : \href{../valid/types.html#valid-fieldtype}{\mathsf{ok}}
}{
C \href{../valid/types.html#valid-comptype}{\vdash} \href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~{\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}} : \href{../valid/types.html#valid-comptype}{\mathsf{ok}}
}
\qquad
\end{array}\]
Field Types
\(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}~\href{../syntax/types.html#syntax-storagetype}{\mathit{storagetype}}\)
\[\begin{array}{@{}c@{}}\displaystyle
\frac{
C \href{../valid/types.html#valid-storagetype}{\vdash} {\href{../syntax/types.html#syntax-storagetype}{\mathit{storagetype}}} : \href{../valid/types.html#valid-storagetype}{\mathsf{ok}}
}{
C \href{../valid/types.html#valid-fieldtype}{\vdash} {\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}^?}~{\href{../syntax/types.html#syntax-storagetype}{\mathit{storagetype}}} : \href{../valid/types.html#valid-fieldtype}{\mathsf{ok}}
}
\qquad
\end{array}\]
\(\href{../syntax/types.html#syntax-packtype}{\mathit{packtype}}\)
\[\begin{array}{@{}c@{}}\displaystyle
\frac{
}{
C \href{../valid/types.html#valid-packtype}{\vdash} {\href{../syntax/types.html#syntax-packtype}{\mathit{packtype}}} : \href{../valid/types.html#valid-packtype}{\mathsf{ok}}
}
\qquad
\end{array}\]
Recursive Types
Recursive types are validated for a specific type index that denotes the index of the type defined by the recursive group.
\(\href{../syntax/types.html#syntax-rectype}{\mathsf{rec}}~\href{../syntax/types.html#syntax-subtype}{\mathit{subtype}}^\ast\)
\[\begin{array}{@{}c@{}}\displaystyle
\frac{
}{
C \href{../valid/types.html#valid-rectype}{\vdash} \href{../syntax/types.html#syntax-rectype}{\mathsf{rec}}~\epsilon : {\href{../valid/types.html#valid-subtype}{\mathsf{ok}}}{(x)}
}
\qquad
\frac{
C \href{../valid/types.html#valid-subtype}{\vdash} {\href{../syntax/types.html#syntax-subtype}{\mathit{subtype}}}_1 : {\href{../valid/types.html#valid-subtype}{\mathsf{ok}}}{(x)}
\qquad
C \href{../valid/types.html#valid-rectype}{\vdash} \href{../syntax/types.html#syntax-rectype}{\mathsf{rec}}~{{\href{../syntax/types.html#syntax-subtype}{\mathit{subtype}}}^\ast} : {\href{../valid/types.html#valid-subtype}{\mathsf{ok}}}{(x + 1)}
}{
C \href{../valid/types.html#valid-rectype}{\vdash} \href{../syntax/types.html#syntax-rectype}{\mathsf{rec}}~({\href{../syntax/types.html#syntax-subtype}{\mathit{subtype}}}_1~{{\href{../syntax/types.html#syntax-subtype}{\mathit{subtype}}}^\ast}) : {\href{../valid/types.html#valid-subtype}{\mathsf{ok}}}{(x)}
}
\qquad
\end{array}\]
\(\href{../syntax/types.html#syntax-subtype}{\mathsf{sub}}~\href{../syntax/types.html#syntax-subtype}{\mathsf{final}}^?~y^\ast~\href{../syntax/types.html#syntax-comptype}{\mathit{comptype}}\)
The composite type \(\href{../syntax/types.html#syntax-comptype}{\mathit{comptype}}\) must be valid.
The sequence \(y^\ast\) may be no longer than \(1\).
For every type index \(y_i\) in \(y^\ast\):
The type index \(y_i\) must be smaller than \(x\).
The type index \(y_i\) must exist in the context \(C\).
Let \(\href{../syntax/types.html#syntax-subtype}{\mathit{subtype}}_i\) be the unrolling of the defined type \(C.\href{../valid/conventions.html#context}{\mathsf{types}}[y_i]\).
The sub type \(\href{../syntax/types.html#syntax-subtype}{\mathit{subtype}}_i\) must not contain \(\href{../syntax/types.html#syntax-subtype}{\mathsf{final}}\).
Let \(\href{../syntax/types.html#syntax-comptype}{\mathit{comptype}}'_i\) be the composite type in \(\href{../syntax/types.html#syntax-subtype}{\mathit{subtype}}_i\).
The composite type \(\href{../syntax/types.html#syntax-comptype}{\mathit{comptype}}\) must match \(\href{../syntax/types.html#syntax-comptype}{\mathit{comptype}}'_i\).
Then the sub type is valid for the type index \(x\).
\[\begin{split}\begin{array}{@{}c@{}}\displaystyle
\frac{
\begin{array}{@{}c@{}}
{|{x^\ast}|} \leq 1
\qquad
(x < x_0)^\ast
\qquad
({\href{../valid/conventions.html#aux-unroll-deftype}{\mathrm{unroll}}}(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]) = \href{../syntax/types.html#syntax-subtype}{\mathsf{sub}}~{{x'}^\ast}~{\href{../syntax/types.html#syntax-comptype}{\mathit{comptype}}'})^\ast
\\
C \href{../valid/types.html#valid-comptype}{\vdash} {\href{../syntax/types.html#syntax-comptype}{\mathit{comptype}}} : \href{../valid/types.html#valid-comptype}{\mathsf{ok}}
\qquad
(C \href{../valid/matching.html#match-comptype}{\vdash} {\href{../syntax/types.html#syntax-comptype}{\mathit{comptype}}} \href{../valid/matching.html#match-comptype}{\leq} {\href{../syntax/types.html#syntax-comptype}{\mathit{comptype}}'})^\ast
\end{array}
}{
C \href{../valid/types.html#valid-subtype}{\vdash} \href{../syntax/types.html#syntax-subtype}{\mathsf{sub}}~{\href{../syntax/types.html#syntax-subtype}{\mathsf{final}}^?}~{x^\ast}~{\href{../syntax/types.html#syntax-comptype}{\mathit{comptype}}} : {\href{../valid/types.html#valid-subtype}{\mathsf{ok}}}{(x_0)}
}
\qquad
\end{array}\end{split}\]
Note
The side condition on the index ensures that a declared supertype is a previously defined types,
preventing cyclic subtype hierarchies.
Future versions of WebAssembly may allow more than one supertype.
Defined Types
\(\href{../syntax/types.html#syntax-rectype}{\mathit{rectype}}.i\)
The recursive type \(\href{../syntax/types.html#syntax-rectype}{\mathit{rectype}}\) must be valid for some type index \(x\).
Let \(\href{../syntax/types.html#syntax-rectype}{\mathsf{rec}}~\href{../syntax/types.html#syntax-subtype}{\mathit{subtype}}^\ast\) be the defined type \(\href{../syntax/types.html#syntax-rectype}{\mathit{rectype}}\).
The number \(i\) must be smaller than the length of the sequence \(\href{../syntax/types.html#syntax-subtype}{\mathit{subtype}}^\ast\) of sub types.
Then the defined type is valid.
\[\begin{array}{@{}c@{}}\displaystyle
\frac{
C \href{../valid/types.html#valid-rectype}{\vdash} {\href{../syntax/types.html#syntax-rectype}{\mathit{rectype}}} : {\href{../valid/types.html#valid-subtype}{\mathsf{ok}}}{(x)}
\qquad
{\href{../syntax/types.html#syntax-rectype}{\mathit{rectype}}} = \href{../syntax/types.html#syntax-rectype}{\mathsf{rec}}~{{\href{../syntax/types.html#syntax-subtype}{\mathit{subtype}}}^{n}}
\qquad
i < n
}{
C \href{../valid/types.html#valid-deftype}{\vdash} {\href{../syntax/types.html#syntax-rectype}{\mathit{rectype}}} {.} i : \href{../valid/types.html#valid-deftype}{\mathsf{ok}}
}
\qquad
\end{array}\]
Limits
Limits must have meaningful bounds that are within a given range.
\(\{ \href{../syntax/types.html#syntax-limits}{\mathsf{min}}~n, \href{../syntax/types.html#syntax-limits}{\mathsf{max}}~m^? \}\)
The value of \(n\) must not be larger than \(k\).
If the maximum \(m^?\) is not empty, then:
Then the limit is valid within range \(k\).
\[\begin{array}{@{}c@{}}\displaystyle
\frac{
n \leq m \leq k
}{
C \href{../valid/types.html#valid-limits}{\vdash} {}[ n \href{../syntax/types.html#syntax-limits}{\,{..}\,} m ] : k
}
\qquad
\end{array}\]
Table Types
\(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}~\href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}\)
The limits \(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}\) must be valid within range \(2^{32}-1\).
The reference type \(\href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}\) must be valid.
Then the table type is valid.
\[\begin{array}{@{}c@{}}\displaystyle
\frac{
C \href{../valid/types.html#valid-limits}{\vdash} {\href{../syntax/types.html#syntax-limits}{\mathit{limits}}} : {2^{32}} - 1
\qquad
C \href{../valid/types.html#valid-reftype}{\vdash} {\href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}} : \href{../valid/types.html#valid-reftype}{\mathsf{ok}}
}{
C \href{../valid/types.html#valid-tabletype}{\vdash} {\href{../syntax/types.html#syntax-limits}{\mathit{limits}}}~{\href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}} : \href{../valid/types.html#valid-tabletype}{\mathsf{ok}}
}
\qquad
\end{array}\]
Memory Types
\(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}\)
\[\begin{array}{@{}c@{}}\displaystyle
\frac{
C \href{../valid/types.html#valid-limits}{\vdash} {\href{../syntax/types.html#syntax-limits}{\mathit{limits}}} : {2^{16}}
}{
C \href{../valid/types.html#valid-memtype}{\vdash} {\href{../syntax/types.html#syntax-limits}{\mathit{limits}}}~\href{../syntax/types.html#syntax-memtype}{\mathsf{page}} : \href{../valid/types.html#valid-memtype}{\mathsf{ok}}
}
\qquad
\end{array}\]
Tag Types
\([t_1^n] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [t_2^m]\)
The function type \([t_1^n] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [t_2^m]\) must be valid.
The type sequence \(t_2^m\) must be empty.
Then the tag type is valid.
\[\begin{array}{@{}c@{}}\displaystyle
\frac{
C \href{../valid/types.html#valid-deftype}{\vdash} {\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}} : \href{../valid/types.html#valid-deftype}{\mathsf{ok}}
\qquad
{\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}} \href{../valid/conventions.html#aux-expand-deftype}{\approx} \href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~{\href{../syntax/types.html#syntax-functype}{\mathit{functype}}}
}{
C \href{../valid/types.html#valid-tagtype}{\vdash} {\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}} : \href{../valid/types.html#valid-tagtype}{\mathsf{ok}}
}
\qquad
\end{array}\]
Global Types
\(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}~\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}\)
\[\begin{array}{@{}c@{}}\displaystyle
\frac{
C \href{../valid/types.html#valid-valtype}{\vdash} t : \href{../valid/types.html#valid-valtype}{\mathsf{ok}}
}{
C \href{../valid/types.html#valid-globaltype}{\vdash} {\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}^?}~t : \href{../valid/types.html#valid-globaltype}{\mathsf{ok}}
}
\qquad
\end{array}\]
External Types
\(\href{../syntax/types.html#syntax-externtype}{\mathsf{func}}~\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}\)
The defined type \(\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}\) must be valid.
The defined type \(\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}\) must be a function type.
Then the external type is valid.
\[\begin{array}{@{}c@{}}\displaystyle
\frac{
C \href{../valid/types.html#valid-deftype}{\vdash} {\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}} : \href{../valid/types.html#valid-deftype}{\mathsf{ok}}
\qquad
{\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}} \href{../valid/conventions.html#aux-expand-deftype}{\approx} \href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~{\href{../syntax/types.html#syntax-functype}{\mathit{functype}}}
}{
C \href{../valid/types.html#valid-externtype}{\vdash} \href{../syntax/types.html#syntax-externtype}{\mathsf{func}}~{\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}} : \href{../valid/types.html#valid-externtype}{\mathsf{ok}}
}
\qquad
\end{array}\]
\(\href{../syntax/types.html#syntax-externtype}{\mathsf{table}}~\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}\)
\[\begin{array}{@{}c@{}}\displaystyle
\frac{
C \href{../valid/types.html#valid-tabletype}{\vdash} {\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}} : \href{../valid/types.html#valid-tabletype}{\mathsf{ok}}
}{
C \href{../valid/types.html#valid-externtype}{\vdash} \href{../syntax/types.html#syntax-externtype}{\mathsf{table}}~{\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}} : \href{../valid/types.html#valid-externtype}{\mathsf{ok}}
}
\qquad
\end{array}\]
\(\href{../syntax/types.html#syntax-externtype}{\mathsf{mem}}~\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}\)
\[\begin{array}{@{}c@{}}\displaystyle
\frac{
C \href{../valid/types.html#valid-memtype}{\vdash} {\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}} : \href{../valid/types.html#valid-memtype}{\mathsf{ok}}
}{
C \href{../valid/types.html#valid-externtype}{\vdash} \href{../syntax/types.html#syntax-externtype}{\mathsf{mem}}~{\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}} : \href{../valid/types.html#valid-externtype}{\mathsf{ok}}
}
\qquad
\end{array}\]
\(\href{../syntax/types.html#syntax-tagtype}{\mathsf{tag}}~\href{../syntax/types.html#syntax-tagtype}{\mathit{tagtype}}\)
\[\begin{array}{@{}c@{}}\displaystyle
\frac{
C \href{../valid/types.html#valid-tagtype}{\vdash} {\href{../syntax/types.html#syntax-tagtype}{\mathit{tagtype}}} : \href{../valid/types.html#valid-tagtype}{\mathsf{ok}}
}{
C \href{../valid/types.html#valid-externtype}{\vdash} \href{../syntax/types.html#syntax-tagtype}{\mathsf{tag}}~{\href{../syntax/types.html#syntax-tagtype}{\mathit{tagtype}}} : \href{../valid/types.html#valid-externtype}{\mathsf{ok}}
}
\qquad
\end{array}\]
\(\href{../syntax/types.html#syntax-externtype}{\mathsf{global}}~\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}\)
\[\begin{array}{@{}c@{}}\displaystyle
\frac{
C \href{../valid/types.html#valid-globaltype}{\vdash} {\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}} : \href{../valid/types.html#valid-globaltype}{\mathsf{ok}}
}{
C \href{../valid/types.html#valid-externtype}{\vdash} \href{../syntax/types.html#syntax-externtype}{\mathsf{global}}~{\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}} : \href{../valid/types.html#valid-externtype}{\mathsf{ok}}
}
\qquad
\end{array}\]