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
1. Pre-condition: :math:`\module` is :ref:`valid <valid-module>` with the external import types :math:`\externtype^\ast` and external export types :math:`{\externtype'}^\ast`.
195
195
196
-
2. Let :math:`\import^\ast` be the :ref:`imports <syntax-import>` of :math:`\module`.
196
+
2. Let :math:`\importmod^\ast` be the :ref:`import modules <syntax-importmod>` of :math:`\module`.
197
197
198
-
3. Assert: the length of :math:`\import^\ast` equals the length of :math:`\externtype^\ast`.
198
+
3. Assert: the sum of the lengths of the items of :math:`\importmod^\ast` equals the length of :math:`\externtype^\ast`.
199
199
200
-
4. For each :math:`\import_i` in :math:`\import^\ast` and corresponding :math:`\externtype_i` in :math:`\externtype^\ast`, do:
200
+
4. Let :math:`n = 0`.
201
201
202
-
a. Let :math:`\IMPORT~\X{nm}_{i1}~\X{nm}_{i2}~\X{xt}_i` be the deconstruction of :math:`\import_i`.
202
+
5. For each :math:`\importmod_i` in :math:`\importmod^\ast`:
203
203
204
-
b. Let :math:`\X{result}_i` be the triple :math:`(\X{nm}_{i1}, \X{nm}_{i2}, \externtype_i)`.
204
+
a. Let :math:`\IMPORTMOD~\X{nm}_1~\X{imports}` be the deconstruction of :math:`\importmod_i`.
205
205
206
-
5. Return the concatenation of all :math:`\X{result}_i`, in index order.
206
+
b. For each :math:`\import_j` in :math:`\X{imports}` and corresponding :math:`\externtype_n` in :math:`\externtype^\ast`, do:
207
+
208
+
i. Let :math:`\IMPORT~\X{nm}_2~\X{xt}_j` be the deconstruction of :math:`\import_j`.
209
+
210
+
ii. Let :math:`\X{resultimport}_n` be the pair :math:`(\X{nm}_2, \externtype_n)`.
211
+
212
+
iii. Increment :math:`n`.
213
+
214
+
c. Let :math:`\X{result}_i` be the pair :math:`(\X{nm}_1, \X{resultimports})`, where :math:`\X{resultimports}` is the concatenation of all :math:`\X{resultimport}_i`, in index order.
215
+
216
+
6. Return the concatenation of all :math:`\X{result}_i`, in index order.
207
217
208
-
6. Post-condition: each :math:`\externtype_i` is :ref:`valid <valid-externtype>` under the empty :ref:`context <context>`.
218
+
7. Post-condition: each :math:`\externtype_i` is :ref:`valid <valid-externtype>` under the empty :ref:`context <context>`.
0 commit comments