You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Copy file name to clipboardExpand all lines: document/core/valid/modules.rst
+2-5Lines changed: 2 additions & 5 deletions
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -740,9 +740,6 @@ that is, its components can only refer to definitions that appear in the module
740
740
Consequently, no initial :ref:`context <context>` is required.
741
741
Instead, the context :math:`C` for validation of the module's content is constructed from the definitions in the module.
742
742
743
-
The :ref:`external types <syntax-externtype>` classifying a module may contain free :ref:`type indices <syntax-typeidx>` that refer to types defined within the module.
744
-
745
-
746
743
* Let :math:`\module` be the module to validate.
747
744
748
745
* The :ref:`types <syntax-type>` :math:`\module.\MTYPES` must be :ref:`valid <valid-type>` yielding a :ref:`context <context>` :math:`C_0`.
@@ -845,7 +842,7 @@ The :ref:`external types <syntax-externtype>` classifying a module may contain f
845
842
846
843
* All export names :math:`\export_i.\ENAME` must be different.
847
844
848
-
* Then the module is valid with :ref:`external types <syntax-externtype>` :math:`\X{it}^\ast\to\X{et}^\ast`.
845
+
* Then the module is valid with :ref:`external types <syntax-externtype>` :math:`\clostype_C(\X{it}^\ast\to\X{et}^\ast)`.
849
846
850
847
.. math::
851
848
\frac{
@@ -913,7 +910,7 @@ The :ref:`external types <syntax-externtype>` classifying a module may contain f
0 commit comments