diff --git a/document/core/binary/modules.rst b/document/core/binary/modules.rst
index 5f99c745a..d2f937a87 100644
--- a/document/core/binary/modules.rst
+++ b/document/core/binary/modules.rst
@@ -139,6 +139,7 @@ $${grammar: {Btypesec Btype}}
    pair: binary format; import
    pair: section; import
 .. _binary-import:
+.. _binary-imports:
 .. _binary-importdesc:
 .. _binary-importsec:
 
@@ -148,7 +149,10 @@ Import Section
 The *import section* has the id 2.
 It decodes into the list of :ref:`imports <syntax-import>` of a :ref:`module <syntax-module>`.
 
-$${grammar: {Bimportsec Bimport}}
+$${grammar: {Bimportsec Bimports Bimport}}
+
+.. note::
+   The encoding of :ref:`imports <binary-imports>` beginning with ${:0x01 0xFF} allows multiple imports to be expressed without repeating the module name. ${:0x01 0xFF} decodes as an invalid :ref:`name <binary-name>` for compatibility with older implementations.
 
 
 .. index:: ! function section, function, type index, function type
diff --git a/document/core/text/modules.rst b/document/core/text/modules.rst
index 167b4f451..f222e83f9 100644
--- a/document/core/text/modules.rst
+++ b/document/core/text/modules.rst
@@ -344,6 +344,7 @@ $${grammar: Tstart_}
 .. index:: import, name, tag type, global type, memory type, table type, function type
    pair: text format; import
 .. _text-import:
+.. _text-imports:
 
 Imports
 ~~~~~~~
@@ -356,7 +357,11 @@ $${grammar: Timport_/plain}
 Abbreviations
 .............
 
-As an abbreviation, imports may also be specified inline with
+Multiple imports with the same ${:nm_1} may be declared together:
+
+$${grammar: Timports_/abbrev}
+
+Imports may also be specified inline with
 :ref:`tag <text-tag>`,
 :ref:`global <text-global>`,
 :ref:`memory <text-mem>`,
diff --git a/document/core/util/macros.def b/document/core/util/macros.def
index 00b8213d3..148fb3061 100644
--- a/document/core/util/macros.def
+++ b/document/core/util/macros.def
@@ -887,6 +887,7 @@
 .. |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}}
+.. |Bimports| mathdef:: \xref{binary/modules}{binary-imports}{\B{imports}}
 .. |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}}
@@ -1071,6 +1072,7 @@
 .. |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}}
+.. |Timports| mathdef:: \xref{text/modules}{text-imports}{\T{imports}}
 .. |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}}
diff --git a/specification/wasm-3.0/5.4-binary.modules.spectec b/specification/wasm-3.0/5.4-binary.modules.spectec
index 6a0900aab..cc33191cc 100644
--- a/specification/wasm-3.0/5.4-binary.modules.spectec
+++ b/specification/wasm-3.0/5.4-binary.modules.spectec
@@ -31,11 +31,15 @@ grammar Btypesec : type* hint(desc "type section") =
 
 ;; Import section
 
-grammar Bimport : import =
-  | nm_1:Bname nm_2:Bname xt:Bexterntype => IMPORT nm_1 nm_2 xt
+grammar Bimport : (name, externtype) =
+  | nm_2:Bname xt:Bexterntype => (nm_2, xt)
+
+grammar Bimports : import* =
+  | nm_1:Bname (nm_2, xt):Bimport => IMPORT nm_1 nm_2 xt
+  | 0x01 0xFF nm_1:Bname (nm_2, xt)*:Blist(Bimport) => (IMPORT nm_1 nm_2 xt)*
 
 grammar Bimportsec : import* hint(desc "import section") =
-  | im*:Bsection_(2, Blist(Bimport)) => im*
+  | im**:Bsection_(2, Blist(Bimports)) => $concat_(import, im**)
 
 
 ;; Function section
diff --git a/specification/wasm-3.0/6.3-text.modules.spectec b/specification/wasm-3.0/6.3-text.modules.spectec
index 48e877ad8..7cee6a76a 100644
--- a/specification/wasm-3.0/6.3-text.modules.spectec
+++ b/specification/wasm-3.0/6.3-text.modules.spectec
@@ -134,6 +134,10 @@ grammar Timport_(I)/plain : (import, idctxt) =
   | "(" "import" nm_1:Tname nm_2:Tname (xt,I'):Texterntype_(I) ")" => (IMPORT nm_1 nm_2 xt, I')
   | ...
 
+grammar Timports_(I)/abbrev : (import*, idctxt) =
+  | "(" "import" nm_1:Tname ("(" "item" nm_2:Tname Texterntype_(I) ")")* ")" ==
+    ("(" "import" nm_1:Tname nm_2:Tname Texterntype_(I) ")")*
+
 grammar Timport_(I)/abbrev-tag : (import, idctxt) = ...
   | "(" "tag" Tid? "(" "import" Tname^2 ")" Ttagtype_(I) ")" ==
     "(" "import" Tname^2 "(" "tag" Tid? Ttagtype_(I) ")" ")"
@@ -158,7 +162,6 @@ grammar Timport_(I)/abbrev-func : (import, idctxt) = ...
   | "(" "func" Tid? "(" "import" Tname^2 ")" Ttypeuse_(I) ")" ==
     "(" "import" Tname^2 "(" "func" Tid? Ttypeuse_(I) ")" ")"
 
-
 ;; Exports
 
 grammar Texport_(I) : (export, idctxt) =
diff --git a/spectec/doc/example/output/NanoWasm.pdf b/spectec/doc/example/output/NanoWasm.pdf
index 3401b402b..2a0cbb015 100644
Binary files a/spectec/doc/example/output/NanoWasm.pdf and b/spectec/doc/example/output/NanoWasm.pdf differ
diff --git a/spectec/test-frontend/TEST.md b/spectec/test-frontend/TEST.md
index 1daf35ebd..c96071b60 100644
--- a/spectec/test-frontend/TEST.md
+++ b/spectec/test-frontend/TEST.md
@@ -8708,14 +8708,21 @@ grammar Btypesec : type*
   prod{`ty*` : type*} ty*{ty <- `ty*`}:Bsection_(1, syntax type, grammar Blist(syntax type, grammar Btype)) => ty*{ty <- `ty*`}
 
 ;; ../../../../specification/wasm-3.0/5.4-binary.modules.spectec
-grammar Bimport : import
+grammar Bimport : (name, externtype)
   ;; ../../../../specification/wasm-3.0/5.4-binary.modules.spectec
-  prod{nm_1 : name, nm_2 : name, xt : externtype} {{nm_1:Bname} {nm_2:Bname} {xt:Bexterntype}} => IMPORT_import(nm_1, nm_2, xt)
+  prod{nm_2 : name, xt : externtype} {{nm_2:Bname} {xt:Bexterntype}} => (nm_2, xt)
+
+;; ../../../../specification/wasm-3.0/5.4-binary.modules.spectec
+grammar Bimports : import*
+  ;; ../../../../specification/wasm-3.0/5.4-binary.modules.spectec
+  prod{nm_1 : name, nm_2 : name, xt : externtype} {{nm_1:Bname} {(nm_2, xt):Bimport}} => [IMPORT_import(nm_1, nm_2, xt)]
+  ;; ../../../../specification/wasm-3.0/5.4-binary.modules.spectec
+  prod{nm_1 : name, `nm_2*` : name*, `xt*` : externtype*} {{0x01} {0xFF} {nm_1:Bname} {(nm_2, xt)*{nm_2 <- `nm_2*`, xt <- `xt*`}:Blist(syntax (name, externtype), grammar Bimport)}} => IMPORT_import(nm_1, nm_2, xt)*{nm_2 <- `nm_2*`, xt <- `xt*`}
 
 ;; ../../../../specification/wasm-3.0/5.4-binary.modules.spectec
 grammar Bimportsec : import*
   ;; ../../../../specification/wasm-3.0/5.4-binary.modules.spectec
-  prod{`im*` : import*} im*{im <- `im*`}:Bsection_(2, syntax import, grammar Blist(syntax import, grammar Bimport)) => im*{im <- `im*`}
+  prod{`im**` : import**} im*{im <- `im*`}*{`im*` <- `im**`}:Bsection_(2, syntax import*, grammar Blist(syntax import*, grammar Bimports)) => $concat_(syntax import, im*{im <- `im*`}*{`im*` <- `im**`})
 
 ;; ../../../../specification/wasm-3.0/5.4-binary.modules.spectec
 grammar Bfuncsec : typeidx*
@@ -10863,6 +10870,9 @@ grammar Tstart_(I : I) : (start, idctxt)
   ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
   prod{x : idx} {{"("} {"start"} {x:Tfuncidx_(I)} {")"}} => (START_start(x), {TYPES [], TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [], DATAS [], ELEMS [], LOCALS [], LABELS [], FIELDS [], TYPEDEFS []})
 
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
+grammar Timports_(I : I) : (import*, idctxt)
+
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 grammar Timport_(I : I) : (import, idctxt)
   ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
@@ -10963,13 +10973,13 @@ syntax decl =
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:258.1-258.76
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:261.1-261.76
 def $typesd(decl*) : type*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:270.1-270.23
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:273.1-273.23
   def $typesd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:271.1-271.48
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:274.1-274.48
   def $typesd{type : type, `decl'*` : decl*}([(type : type <: decl)] ++ decl'*{decl' <- `decl'*`}) = [type] ++ $typesd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:272.1-272.57
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:275.1-275.57
   def $typesd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $typesd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -10977,13 +10987,13 @@ def $typesd(decl*) : type*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:259.1-259.78
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:262.1-262.78
 def $importsd(decl*) : import*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:274.1-274.25
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:277.1-277.25
   def $importsd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:275.1-275.56
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:278.1-278.56
   def $importsd{import : import, `decl'*` : decl*}([(import : import <: decl)] ++ decl'*{decl' <- `decl'*`}) = [import] ++ $importsd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:276.1-276.61
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:279.1-279.61
   def $importsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $importsd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -10991,13 +11001,13 @@ def $importsd(decl*) : import*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:260.1-260.75
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:263.1-263.75
 def $tagsd(decl*) : tag*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:278.1-278.22
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:281.1-281.22
   def $tagsd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:279.1-279.44
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:282.1-282.44
   def $tagsd{tag : tag, `decl'*` : decl*}([(tag : tag <: decl)] ++ decl'*{decl' <- `decl'*`}) = [tag] ++ $tagsd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:280.1-280.55
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:283.1-283.55
   def $tagsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $tagsd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -11005,13 +11015,13 @@ def $tagsd(decl*) : tag*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:261.1-261.78
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:264.1-264.78
 def $globalsd(decl*) : global*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:282.1-282.25
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:285.1-285.25
   def $globalsd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:283.1-283.56
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:286.1-286.56
   def $globalsd{global : global, `decl'*` : decl*}([(global : global <: decl)] ++ decl'*{decl' <- `decl'*`}) = [global] ++ $globalsd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:284.1-284.61
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:287.1-287.61
   def $globalsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $globalsd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -11019,13 +11029,13 @@ def $globalsd(decl*) : global*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:262.1-262.75
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:265.1-265.75
 def $memsd(decl*) : mem*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:286.1-286.22
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:289.1-289.22
   def $memsd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:287.1-287.44
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:290.1-290.44
   def $memsd{mem : mem, `decl'*` : decl*}([(mem : mem <: decl)] ++ decl'*{decl' <- `decl'*`}) = [mem] ++ $memsd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:288.1-288.55
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:291.1-291.55
   def $memsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $memsd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -11033,13 +11043,13 @@ def $memsd(decl*) : mem*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:263.1-263.77
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:266.1-266.77
 def $tablesd(decl*) : table*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:290.1-290.24
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:293.1-293.24
   def $tablesd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:291.1-291.52
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:294.1-294.52
   def $tablesd{table : table, `decl'*` : decl*}([(table : table <: decl)] ++ decl'*{decl' <- `decl'*`}) = [table] ++ $tablesd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:292.1-292.59
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:295.1-295.59
   def $tablesd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $tablesd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -11047,13 +11057,13 @@ def $tablesd(decl*) : table*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:264.1-264.76
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:267.1-267.76
 def $funcsd(decl*) : func*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:294.1-294.23
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:297.1-297.23
   def $funcsd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:295.1-295.48
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:298.1-298.48
   def $funcsd{func : func, `decl'*` : decl*}([(func : func <: decl)] ++ decl'*{decl' <- `decl'*`}) = [func] ++ $funcsd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:296.1-296.57
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:299.1-299.57
   def $funcsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $funcsd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -11061,13 +11071,13 @@ def $funcsd(decl*) : func*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:265.1-265.76
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:268.1-268.76
 def $datasd(decl*) : data*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:298.1-298.23
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:301.1-301.23
   def $datasd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:299.1-299.48
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:302.1-302.48
   def $datasd{data : data, `decl'*` : decl*}([(data : data <: decl)] ++ decl'*{decl' <- `decl'*`}) = [data] ++ $datasd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:300.1-300.57
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:303.1-303.57
   def $datasd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $datasd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -11075,13 +11085,13 @@ def $datasd(decl*) : data*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:266.1-266.76
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:269.1-269.76
 def $elemsd(decl*) : elem*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:302.1-302.23
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:305.1-305.23
   def $elemsd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:303.1-303.48
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:306.1-306.48
   def $elemsd{elem : elem, `decl'*` : decl*}([(elem : elem <: decl)] ++ decl'*{decl' <- `decl'*`}) = [elem] ++ $elemsd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:304.1-304.57
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:307.1-307.57
   def $elemsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $elemsd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -11089,13 +11099,13 @@ def $elemsd(decl*) : elem*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:267.1-267.77
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:270.1-270.77
 def $startsd(decl*) : start*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:306.1-306.24
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:309.1-309.24
   def $startsd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:307.1-307.52
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:310.1-310.52
   def $startsd{start : start, `decl'*` : decl*}([(start : start <: decl)] ++ decl'*{decl' <- `decl'*`}) = [start] ++ $startsd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:308.1-308.59
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:311.1-311.59
   def $startsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $startsd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -11103,13 +11113,13 @@ def $startsd(decl*) : start*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:268.1-268.78
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:271.1-271.78
 def $exportsd(decl*) : export*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:310.1-310.25
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:313.1-313.25
   def $exportsd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:311.1-311.56
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:314.1-314.56
   def $exportsd{export : export, `decl'*` : decl*}([(export : export <: decl)] ++ decl'*{decl' <- `decl'*`}) = [export] ++ $exportsd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:312.1-312.61
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:315.1-315.61
   def $exportsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $exportsd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
diff --git a/spectec/test-latex/TEST.md b/spectec/test-latex/TEST.md
index ba981cc99..15cc55116 100644
--- a/spectec/test-latex/TEST.md
+++ b/spectec/test-latex/TEST.md
@@ -12024,8 +12024,10 @@ $$
 
 $$
 \begin{array}[t]{@{}lrrl@{}l@{}l@{}l@{}}
-& {\mathtt{import}} & ::= & {\mathit{nm}}_1{:}{\mathtt{name}}~~{\mathit{nm}}_2{:}{\mathtt{name}}~~{\mathit{xt}}{:}{\mathtt{externtype}} & \quad\Rightarrow\quad{} & \mathsf{import}~{\mathit{nm}}_1~{\mathit{nm}}_2~{\mathit{xt}} \\
-\mbox{(import section)} & {\mathtt{importsec}} & ::= & {{\mathit{im}}^\ast}{:}{{\mathtt{section}}}_{2}({\mathtt{list}}({\mathtt{import}})) & \quad\Rightarrow\quad{} & {{\mathit{im}}^\ast} \\
+& {\mathtt{import}} & ::= & {\mathit{nm}}_2{:}{\mathtt{name}}~~{\mathit{xt}}{:}{\mathtt{externtype}} & \quad\Rightarrow\quad{} & ({\mathit{nm}}_2, {\mathit{xt}}) \\
+& {\mathtt{imports}} & ::= & {\mathit{nm}}_1{:}{\mathtt{name}}~~({\mathit{nm}}_2, {\mathit{xt}}){:}{\mathtt{import}} & \quad\Rightarrow\quad{} & \mathsf{import}~{\mathit{nm}}_1~{\mathit{nm}}_2~{\mathit{xt}} \\
+& & | & \mathtt{0x01}~~\mathtt{0xFF}~~{\mathit{nm}}_1{:}{\mathtt{name}}~~{({\mathit{nm}}_2, {\mathit{xt}})^\ast}{:}{\mathtt{list}}({\mathtt{import}}) & \quad\Rightarrow\quad{} & {(\mathsf{import}~{\mathit{nm}}_1~{\mathit{nm}}_2~{\mathit{xt}})^\ast} \\
+\mbox{(import section)} & {\mathtt{importsec}} & ::= & {{{\mathit{im}}^\ast}^\ast}{:}{{\mathtt{section}}}_{2}({\mathtt{list}}({\mathtt{imports}})) & \quad\Rightarrow\quad{} & {\bigoplus}\, {{{\mathit{im}}^\ast}^\ast} \\
 \end{array}
 $$
 
@@ -13581,6 +13583,13 @@ $$
 $$
 \begin{array}[t]{@{}lrrl@{}l@{}l@{}l@{}}
 & {{\mathtt{import}}}_{I} & ::= & \mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{import}’}~~{\mathit{nm}}_1{:}{\mathtt{name}}~~{\mathit{nm}}_2{:}{\mathtt{name}}~~({\mathit{xt}}, {I'}){:}{{\mathtt{externtype}}}_{I}~~\mbox{‘\texttt{{)}}’} & \quad\Rightarrow\quad{} & (\mathsf{import}~{\mathit{nm}}_1~{\mathit{nm}}_2~{\mathit{xt}}, {I'}) \\
+& {{\mathtt{imports}}}_{I} & ::= & \mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{import}’}~~{\mathit{nm}}_1{:}{\mathtt{name}}~~{(\mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{item}’}~~{\mathit{nm}}_2{:}{\mathtt{name}}~~{{\mathtt{externtype}}}_{I}~~\mbox{‘\texttt{{)}}’})^\ast}~~\mbox{‘\texttt{{)}}’} & \quad\equiv\quad{} & & \\
+&&& \multicolumn{4}{@{}l@{}}{\quad
+\begin{array}[t]{@{}l@{}}
+{(\mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{import}’}~~{\mathit{nm}}_1{:}{\mathtt{name}}~~{\mathit{nm}}_2{:}{\mathtt{name}}~~{{\mathtt{externtype}}}_{I}~~\mbox{‘\texttt{{)}}’})^\ast} \\
+\end{array}
+} \\
+& {{\mathtt{import}}}_{I} & ::= & \dots \\
 & & | & \mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{tag}’}~~{{\mathtt{id}}^?}~~\mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{import}’}~~{{\mathtt{name}}^{2}}~~\mbox{‘\texttt{{)}}’}~~{{\mathtt{tagtype}}}_{I}~~\mbox{‘\texttt{{)}}’} & \quad\equiv\quad{} & & \\
 &&& \multicolumn{4}{@{}l@{}}{\quad
 \begin{array}[t]{@{}l@{}}
diff --git a/spectec/test-latex/test-test.el b/spectec/test-latex/test-test.el
new file mode 100644
index 000000000..3c8bbed6a
--- /dev/null
+++ b/spectec/test-latex/test-test.el
@@ -0,0 +1,611 @@
+== Parsing...
+var XYZ : nat
+def $test_sub_ATOM_22(nat : nat) : nat
+def $test_sub_ATOM_22(n_1_xyz_y) = 0
+def $test_sub_ATOM_22(n_2_XYZ_y) = 0
+def $test_sub_ATOM_22(n_3_ATOM_y) = 0
+def $curried_(nat : nat, nat : nat) : nat
+def $curried_(n_1, n_2) = n_1 + n_2
+syntax testfuse = | {AB_ nat nat nat} | {CD nat nat nat} | {EF nat nat nat} | {GH nat nat nat} | {IJ nat nat nat} | {KL nat nat nat} | {MN nat nat nat} | {OP nat nat nat} | {QR nat nat nat}
+
+
+
+syntax InfixArrow = | nat* ->_ {(nat*) nat*}
+syntax InfixArrow2 = | nat* =>_ {(nat*) nat*}
+syntax AtomArrow = {nat? ->_ (nat*) nat*}
+syntax AtomArrow2 = {nat? =>_ (nat*) nat*}
+def $InfixArrow(InfixArrow : InfixArrow) : nat
+def $InfixArrow(a ->_ c) = 0
+def $InfixArrow(a ->_ {c b}) = 0
+def $InfixArrow(a ->_ {(c*) b}) = 0
+def $InfixArrow(a ->_ {c b_1 b_2}) = 0
+def $InfixArrow(a ->_ {(c*) b_1 b_2}) = 0
+def $InfixArrow(a ->_ {({c_1 c_2}) b_1 b_2}) = 0
+def $InfixArrow({} ->_ {({c_1 c_2}) b_1 b_2}) = 0
+def $InfixArrow2(InfixArrow2 : InfixArrow2) : nat
+def $InfixArrow2(a =>_ c) = 0
+def $InfixArrow2(a =>_ {c b}) = 0
+def $InfixArrow2(a =>_ {(c*) b}) = 0
+def $InfixArrow2(a =>_ {c b_1 b_2}) = 0
+def $InfixArrow2(a =>_ {(c*) b_1 b_2}) = 0
+def $InfixArrow2(a =>_ {({c_1 c_2}) b_1 b_2}) = 0
+def $InfixArrow2({} =>_ {({c_1 c_2}) b_1 b_2}) = 0
+def $AtomArrow(AtomArrow : AtomArrow) : nat
+def $AtomArrow({a ->_ c}) = 0
+def $AtomArrow({a ->_ c b}) = 0
+def $AtomArrow({a ->_ (c*) b}) = 0
+def $AtomArrow({a ->_ c b_1 b_2}) = 0
+def $AtomArrow({a ->_ (c*) b_1 b_2}) = 0
+def $AtomArrow({a ->_ ({c_1 c_2}) b_1 b_2}) = 0
+def $AtomArrow({->_ ({c_1 c_2}) b_1 b_2}) = 0
+def $AtomArrow2(AtomArrow2 : AtomArrow2) : nat
+def $AtomArrow2({a =>_ c}) = 0
+def $AtomArrow2({a =>_ c b}) = 0
+def $AtomArrow2({a =>_ (c*) b}) = 0
+def $AtomArrow2({a =>_ c b_1 b_2}) = 0
+def $AtomArrow2({a =>_ (c*) b_1 b_2}) = 0
+def $AtomArrow2({a =>_ ({c_1 c_2}) b_1 b_2}) = 0
+def $AtomArrow2({=>_ ({c_1 c_2}) b_1 b_2}) = 0
+syntax MacroInfixArrow = | nat* ->_ {nat* nat*}
+syntax MacroAtomArrow = | nat* ->_ {nat* nat*}
+def $MacroInfixArrow(MacroInfixArrow : MacroInfixArrow) : nat
+def $MacroInfixArrow(a ->_ c) = 0
+def $MacroInfixArrow(a ->_ {c b}) = 0
+def $MacroInfixArrow(a ->_ {(c*) b}) = 0
+def $MacroInfixArrow(a ->_ {c b_1 b_2}) = 0
+def $MacroInfixArrow(a ->_ {(c*) b_1 b_2}) = 0
+def $MacroInfixArrow(a ->_ {({c_1 c_2}) b_1 b_2}) = 0
+def $MacroInfixArrow({} ->_ {({c_1 c_2}) b_1 b_2}) = 0
+def $MacroAtomArrow(MacroAtomArrow : MacroAtomArrow) : nat
+def $MacroAtomArrow(a ->_ c) = 0
+def $MacroAtomArrow(a ->_ {c b}) = 0
+def $MacroAtomArrow(a ->_ {(c*) b}) = 0
+def $MacroAtomArrow(a ->_ {c b_1 b_2}) = 0
+def $MacroAtomArrow(a ->_ {(c*) b_1 b_2}) = 0
+def $MacroAtomArrow(a ->_ {({c_1 c_2}) b_1 b_2}) = 0
+def $MacroAtomArrow({} ->_ {({c_1 c_2}) b_1 b_2}) = 0
+syntax ShowInfixArrow = | nat* ->_ {nat* nat*}
+syntax ShowAtomArrow = | nat* ->_ {nat* nat*}
+def $ShowInfixArrow(ShowInfixArrow : ShowInfixArrow) : nat
+def $ShowInfixArrow(a ->_ c) = 0
+def $ShowInfixArrow(a ->_ {c b}) = 0
+def $ShowInfixArrow(a ->_ {(c*) b}) = 0
+def $ShowInfixArrow(a ->_ {c b_1 b_2}) = 0
+def $ShowInfixArrow(a ->_ {(c*) b_1 b_2}) = 0
+def $ShowInfixArrow(a ->_ {({c_1 c_2}) b_1 b_2}) = 0
+def $ShowInfixArrow({} ->_ {({c_1 c_2}) b_1 b_2}) = 0
+def $ShowAtomArrow(ShowAtomArrow : ShowAtomArrow) : nat
+def $ShowAtomArrow(a ->_ c) = 0
+def $ShowAtomArrow(a ->_ {c b}) = 0
+def $ShowAtomArrow(a ->_ {(c*) b}) = 0
+def $ShowAtomArrow(a ->_ {c b_1 b_2}) = 0
+def $ShowAtomArrow(a ->_ {(c*) b_1 b_2}) = 0
+def $ShowAtomArrow(a ->_ {({c_1 c_2}) b_1 b_2}) = 0
+def $ShowAtomArrow({} ->_ {({c_1 c_2}) b_1 b_2}) = 0
+syntax ShowMacroInfixArrow = | nat* ->_ {nat* nat*}
+syntax ShowMacroAtomArrow = | nat* ->_ {nat* nat*}
+def $ShowMacroInfixArrow(ShowMacroInfixArrow : ShowMacroInfixArrow) : nat
+def $ShowMacroInfixArrow(a ->_ c) = 0
+def $ShowMacroInfixArrow(a ->_ {c b}) = 0
+def $ShowMacroInfixArrow(a ->_ {(c*) b}) = 0
+def $ShowMacroInfixArrow(a ->_ {c b_1 b_2}) = 0
+def $ShowMacroInfixArrow(a ->_ {(c*) b_1 b_2}) = 0
+def $ShowMacroInfixArrow(a ->_ {({c_1 c_2}) b_1 b_2}) = 0
+def $ShowMacroInfixArrow({} ->_ {({c_1 c_2}) b_1 b_2}) = 0
+def $ShowMacroAtomArrow(ShowMacroAtomArrow : ShowMacroAtomArrow) : nat
+def $ShowMacroAtomArrow(a ->_ c) = 0
+def $ShowMacroAtomArrow(a ->_ {c b}) = 0
+def $ShowMacroAtomArrow(a ->_ {(c*) b}) = 0
+def $ShowMacroAtomArrow(a ->_ {c b_1 b_2}) = 0
+def $ShowMacroAtomArrow(a ->_ {(c*) b_1 b_2}) = 0
+def $ShowMacroAtomArrow(a ->_ {({c_1 c_2}) b_1 b_2}) = 0
+def $ShowMacroAtomArrow({} ->_ {({c_1 c_2}) b_1 b_2}) = 0
+
+
+
+
+
+
+syntax xfoo = | XFOONULL | {XFOOUN0 nat} | {XFOOUN1N nat} | {XFOOUN11 nat} | {XFOOUNREST nat} | {XFOOBIN0 nat nat} | {XFOOBIN1N nat nat} | {XFOOBIN11 nat nat} | {XFOOBIN1N2N nat nat} | {XFOOBIN1N22 nat nat} | {XFOOBIN112N nat nat} | {XFOOBIN1122 nat nat} | {XFOOBIN22 nat nat} | {XFOOBIN2211 nat nat} | {XFOOBINREST nat nat} | {XFOOBIN1NREST nat nat} | {XFOOBIN11REST nat nat} | {XFOOBIN22REST nat nat} | {XFOOBIN1N2NREST nat nat} | {XFOOBIN1122REST nat nat} | {XFOOBIN2211REST nat nat} | {XFOONAME1N2NREST nat nat} | {XFOONAME1122REST nat nat} | {XFOONAME2211REST nat nat}
+syntax xxfoo = {xfoo nat}
+syntax xxxfoo = {nat xfoo nat}
+def $xfoo(xfoo : xfoo) : nat
+def $xfoo(XFOONULL) = 0
+def $xfoo({XFOOUN0 2}) = 0
+def $xfoo({XFOOUN1N 2}) = 0
+def $xfoo({XFOOUN11 2}) = 0
+def $xfoo({XFOOUNREST 2}) = 0
+def $xfoo({XFOOBIN0 2 3}) = 0
+def $xfoo({XFOOBIN1N 2 3}) = 0
+def $xfoo({XFOOBIN11 2 3}) = 0
+def $xfoo({XFOOBIN1N2N 2 3}) = 0
+def $xfoo({XFOOBIN1N22 2 3}) = 0
+def $xfoo({XFOOBIN112N 2 3}) = 0
+def $xfoo({XFOOBIN1122 2 3}) = 0
+def $xfoo({XFOOBIN22 2 3}) = 0
+def $xfoo({XFOOBIN2211 2 3}) = 0
+def $xfoo({XFOOBINREST 2 3}) = 0
+def $xfoo({XFOOBIN1NREST 2 3}) = 0
+def $xfoo({XFOOBIN11REST 2 3}) = 0
+def $xfoo({XFOOBIN22REST 2 3}) = 0
+def $xfoo({XFOOBIN1N2NREST 2 3}) = 0
+def $xfoo({XFOOBIN1122REST 2 3}) = 0
+def $xfoo({XFOOBIN2211REST 2 3}) = 0
+def $xfoo({XFOONAME1N2NREST 2 3}) = 0
+def $xfoo({XFOONAME1122REST 2 3}) = 0
+def $xfoo({XFOONAME2211REST 2 3}) = 0
+def $xxfoo(xxfoo : xxfoo) : nat
+def $xxfoo({XFOONULL 9}) = 0
+def $xxxfoo(xxxfoo : xxxfoo) : nat
+def $xxxfoo({1 XFOONULL 9}) = 0
+
+
+
+
+
+
+syntax fii = | FII
+syntax faa = | FAA
+syntax foo = | FOO
+syntax fuu = | FUU
+syntax bar = | BAR
+syntax boo = | BOO
+syntax baz = | BAZ
+syntax boi = | BOI
+def $macros1 : nat
+def $macros1 = 0
+  -- if fii = FII
+  -- if faa = FAA
+  -- if foo = FOO
+  -- if fuu = FUU
+  -- if bar = BAR
+  -- if boo = BOO
+  -- if baz = BAZ
+  -- if boi = BOI
+syntax ufii_(nat_1, nat_2) = | UFII
+syntax ufaa_(nat_1, nat_2) = | UFAA
+syntax ufoo_(nat_1, nat_2) = | UFOO
+syntax ufuu_(nat_1, nat_2) = | UFUU
+syntax ubar_(nat_1, nat_2) = | UBAR
+syntax uboo_(nat_1, nat_2) = | UBOO
+syntax ubaz_(nat_1, nat_2) = | UBAZ
+syntax uboi_(nat_1, nat_2) = | UBOI
+def $macros2 : nat
+def $macros2 = 0
+  -- var ufii: ufii_(0, 0)
+  -- if ufii = UFII
+  -- var ufaa: ufaa_(0, 0)
+  -- if ufaa = UFAA
+  -- var ufoo: ufoo_(0, 0)
+  -- if ufoo = UFOO
+  -- var ufuu: ufuu_(0, 0)
+  -- if ufuu = UFUU
+  -- var ubar: ubar_(0, 0)
+  -- if ubar = UBAR
+  -- var uboo: uboo_(0, 0)
+  -- if uboo = UBOO
+  -- var ubaz: ubaz_(0, 0)
+  -- if ubaz = UBAZ
+  -- var uboi: uboi_(0, 0)
+  -- if uboi = UBOI
+
+
+
+def $fii : nat
+def $fii = 0
+def $faa : nat
+def $faa = 0
+def $foo : nat
+def $foo = 0
+def $fuu : nat
+def $fuu = 0
+def $bar : nat
+def $bar = 0
+def $boo : nat
+def $boo = 0
+def $baz : nat
+def $baz = 0
+def $boi : nat
+def $boi = 0
+def $ufii_(nat_1 : nat, nat_2 : nat) : nat
+def $ufii_(x, y) = 0
+def $ufaa_(nat_1 : nat, nat_2 : nat) : nat
+def $ufaa_(x, y) = 0
+def $ufoo_(nat_1 : nat, nat_2 : nat) : nat
+def $ufoo_(x, y) = 0
+def $ufuu_(nat_1 : nat, nat_2 : nat) : nat
+def $ufuu_(x, y) = 0
+def $ubar_(nat_1 : nat, nat_2 : nat) : nat
+def $ubar_(x, y) = 0
+def $uboo_(nat_1 : nat, nat_2 : nat) : nat
+def $uboo_(x, y) = 0
+def $ubaz_(nat_1 : nat, nat_2 : nat) : nat
+def $ubaz_(x, y) = 0
+def $uboi_(nat_1 : nat, nat_2 : nat) : nat
+def $uboi_(x, y) = 0
+def $foo__bar : nat
+def $foo__bar = 0
+def $foo_boo : nat
+def $foo_boo = 0
+def $ufoo__bar_(nat_1 : nat, nat_2 : nat) : nat
+def $ufoo__bar_(x, y) = 0
+def $ufoo_boo_(nat_1 : nat, nat_2 : nat) : nat
+def $ufoo_boo_(x, y) = 0
+
+
+
+syntax parent = | AA | AAX | AAY | AAZ | BB | BBX | BBY | BBZ | {CC nat CCCC} | {CCX nat CCXX} | {CCY nat CCYY} | {CCZ nat CCZZ} | {DD nat} | {DDX nat} | {DDY nat} | {DDZ nat} | {EE nat} | {EEX nat} | {EEY nat} | {EEZ nat}
+def $parent(parent : parent) : nat
+def $parent(AA) = 0
+def $parent(AAX) = 0
+def $parent(AAY) = 0
+def $parent(AAZ) = 0
+def $parent(BB) = 0
+def $parent(BBX) = 0
+def $parent(BBY) = 0
+def $parent(BBZ) = 0
+def $parent({CC n CCCC}) = 0
+def $parent({CCX n CCXX}) = 0
+def $parent({CCY n CCYY}) = 0
+def $parent({CCZ n CCZZ}) = 0
+def $parent({DD n}) = 0
+def $parent({DDX n}) = 0
+def $parent({DDY n}) = 0
+def $parent({DDZ n}) = 0
+def $parent({EE n}) = 0
+def $parent({EEX n}) = 0
+def $parent({EEY n}) = 0
+def $parent({EEZ n}) = 0
+syntax parentimplicit(syntax t) = | PP | PPX | PPY | PPZ | QQ | QQX | QQY | QQZ | {RR t} | {RRX t} | {RRY t} | {RRZ t}
+def $parentimpl(parentimplicit : parentimplicit(text)) : nat
+def $parentimpl(PP) = 0
+def $parentimpl(PPX) = 0
+def $parentimpl(PPY) = 0
+def $parentimpl(PPZ) = 0
+def $parentimpl(QQ) = 0
+def $parentimpl(QQX) = 0
+def $parentimpl(QQY) = 0
+def $parentimpl(QQZ) = 0
+def $parentimpl({RR n}) = 0
+def $parentimpl({RRX n}) = 0
+def $parentimpl({RRY n}) = 0
+def $parentimpl({RRZ n}) = 0
+syntax indirect = parentimplicit(nat)
+def $indirect(indirect : indirect) : nat
+def $indirect(PP) = 0
+def $indirect(PPX) = 0
+def $indirect(PPY) = 0
+def $indirect(PPZ) = 0
+def $indirect(QQ) = 0
+def $indirect(QQX) = 0
+def $indirect(QQY) = 0
+def $indirect(QQZ) = 0
+def $indirect({RR n}) = 0
+def $indirect({RRX n}) = 0
+def $indirect({RRY n}) = 0
+def $indirect({RRZ n}) = 0
+syntax family(nat : nat)
+syntax family(0) = | FF
+syntax family(1) = | GG
+syntax family(2) = | HH
+def $family(nat : nat, family : family(nat)) : nat
+def $family(0, FF) = 0
+def $family(1, GG) = 0
+def $family(2, HH) = 0
+syntax child = | parent | family(0) | indirect | ZZZ
+def $child(child : child) : nat
+def $child(AA) = 0
+def $child(AAX) = 0
+def $child(AAY) = 0
+def $child(AAZ) = 0
+def $child(BB) = 0
+def $child(BBX) = 0
+def $child(BBY) = 0
+def $child(BBZ) = 0
+def $child({CC n CCCC}) = 0
+def $child({CCX n CCXX}) = 0
+def $child({CCY n CCYY}) = 0
+def $child({CCZ n CCZZ}) = 0
+def $child({DD n}) = 0
+def $child({DDX n}) = 0
+def $child({DDY n}) = 0
+def $child({DDZ n}) = 0
+def $child({EE n}) = 0
+def $child({EEX n}) = 0
+def $child({EEY n}) = 0
+def $child({EEZ n}) = 0
+def $child(FF) = 0
+def $child(PP) = 0
+def $child(PPX) = 0
+def $child(PPY) = 0
+def $child(PPZ) = 0
+def $child(QQ) = 0
+def $child(QQX) = 0
+def $child(QQY) = 0
+def $child(QQZ) = 0
+def $child({RR n}) = 0
+def $child({RRX n}) = 0
+def $child({RRY n}) = 0
+def $child({RRZ n}) = 0
+def $child(ZZZ) = 0
+syntax grandchild = | child | ZZZZ
+def $grandchild(grandchild : grandchild) : nat
+def $grandchild(AA) = 0
+def $grandchild(AAX) = 0
+def $grandchild(AAY) = 0
+def $grandchild(AAZ) = 0
+def $grandchild(BB) = 0
+def $grandchild(BBX) = 0
+def $grandchild(BBY) = 0
+def $grandchild(BBZ) = 0
+def $grandchild({CC n CCCC}) = 0
+def $grandchild({CCX n CCXX}) = 0
+def $grandchild({CCY n CCYY}) = 0
+def $grandchild({CCZ n CCZZ}) = 0
+def $grandchild({DD n}) = 0
+def $grandchild({DDX n}) = 0
+def $grandchild({DDY n}) = 0
+def $grandchild({DDZ n}) = 0
+def $grandchild({EE n}) = 0
+def $grandchild({EEX n}) = 0
+def $grandchild({EEY n}) = 0
+def $grandchild({EEZ n}) = 0
+def $grandchild(FF) = 0
+def $grandchild(PP) = 0
+def $grandchild(PPX) = 0
+def $grandchild(PPY) = 0
+def $grandchild(PPZ) = 0
+def $grandchild(QQ) = 0
+def $grandchild(QQX) = 0
+def $grandchild(QQY) = 0
+def $grandchild(QQZ) = 0
+def $grandchild({RR n}) = 0
+def $grandchild({RRX n}) = 0
+def $grandchild({RRY n}) = 0
+def $grandchild({RRZ n}) = 0
+def $grandchild(ZZZ) = 0
+def $grandchild(ZZZZ) = 0
+
+
+
+syntax rec = {FA nat*, FB nat*, FC nat*, FD nat*, FE nat*, FF nat*, FG nat*, FH nat*}
+def $proj(rec : rec, nat : nat) : nat*
+def $proj(r, 0) = r.FA
+def $proj(r, 1) = r.FB
+def $proj(r, 2) = r.FC
+def $proj(r, 3) = r.FD
+def $proj(r, 4) = r.FE
+def $proj(r, 5) = r.FF
+def $proj(r, 6) = r.FG
+def $proj(r, 7) = r.FH
+def $upd(rec : rec, nat : nat) : rec
+def $upd(r, 0) = r[FA = 0]
+def $upd(r, 1) = r[FB = 0]
+def $upd(r, 2) = r[FC = 0]
+def $upd(r, 3) = r[FD = 0]
+def $upd(r, 4) = r[FE = 0]
+def $upd(r, 5) = r[FF = 0]
+def $upd(r, 6) = r[FG = 0]
+def $upd(r, 7) = r[FH = 0]
+def $ext(rec : rec, nat : nat) : rec
+def $ext(r, 0) = r[FA =++ 0]
+def $ext(r, 1) = r[FB =++ 0]
+def $ext(r, 2) = r[FC =++ 0]
+def $ext(r, 3) = r[FD =++ 0]
+def $ext(r, 4) = r[FE =++ 0]
+def $ext(r, 5) = r[FF =++ 0]
+def $ext(r, 6) = r[FG =++ 0]
+def $ext(r, 7) = r[FH =++ 0]
+syntax recimpl = {FIA nat*, FIB nat*, FIC nat*, FID nat*, FIE nat*, FIF nat*, FIG nat*, FIH nat*}
+def $rproj(recimpl : recimpl, nat : nat) : nat*
+def $rproj(r, 0) = r.FIA
+def $rproj(r, 1) = r.FIB
+def $rproj(r, 2) = r.FIC
+def $rproj(r, 3) = r.FID
+def $rproj(r, 4) = r.FIE
+def $rproj(r, 5) = r.FIF
+def $rproj(r, 6) = r.FIG
+def $rproj(r, 7) = r.FIH
+
+
+
+syntax cona = {nat COA nat}
+syntax conb = {nat COB nat}
+syntax conc = {nat COC nat}
+syntax cond = {nat COD nat}
+syntax cone = {nat COE nat}
+syntax conf = {nat COF nat}
+syntax cong = {nat COG nat}
+syntax conh = {nat COH nat}
+
+
+
+syntax C = {}
+relation Rok: C |- parent : OK
+relation Rsub: C |- parent <: parent
+relation Reval: parent ; child ~> parent ; child
+rule Rok:
+  C |- AA : OK
+rule Rsub:
+  C |- parent <: AA
+rule Reval:
+  parent ; child ~> AA ; BB
+relation Rok_macro: C |- parent : OK
+relation Rsub_macro: C |- parent <: parent
+relation Reval_macro: parent ; child ~> parent ; child
+rule Rok_macro:
+  C |- AA : OK
+rule Rsub_macro:
+  C |- parent <: AA
+rule Reval_macro:
+  parent ; child ~> AA ; BB
+relation Rok_nomacro: C |- parent : OK
+relation Rsub_nomacro: C |- parent <: parent
+relation Reval_nomacro: parent ; child ~> parent ; child
+rule Rok_nomacro:
+  C |- AA : OK
+rule Rsub_nomacro:
+  C |- parent <: AA
+rule Reval_nomacro:
+  parent ; child ~> AA ; BB
+
+
+
+
+
+
+syntax argh = | ARGH
+syntax borg = | BORG
+syntax curb = | CURB
+syntax dork = | DORK
+syntax eerk = | EERK
+
+
+
+syntax dotstypex/1 = | argh | DX1 | ...
+syntax dotstypey/1 = | argh | DY1 | ...
+syntax dotstypex/2 = | ... | borg | DX2 | ...
+syntax dotstypesep = borg
+syntax dotstypex/3 = | ... | curb | DX3 | DX4 | DX5 | DX6 | ...
+syntax dotstypey/2 = | ... | borg | DY2 | DY3 | DY4 | ...
+syntax dotstypex/4 = | ... | dork | DX7
+syntax dotstypey/3 = | ... | dork | DY5
+
+
+
+syntax casetype = | {LA nat argh}
+  -- if nat = 0
+  -- if argh =/= ARGH | {LB borg curb} | {LC dork_1 dork_2}
+  -- if dork_1 =/= dork_2 | {LD argh nat}
+  -- if nat > 0
+  -- if argh =/= ARGH | {LE nat_1 nat_2}
+  -- if nat_1 <= nat_2 | {LFA borg} | {LFB borg} | {LFC borg} | {LH borg argh eerk} | {LI borg argh eerk}
+  -- if 0 < 1
+  -- if 1 > 0 | {LJ borg}
+  -- if 0 < 1
+  -- if 1 > 0 | {LK borg argh eerk}
+  -- if 0 < 1
+  -- if 1 > 0
+
+
+
+grammar gram : nat* = 
+  | {"GA" "GB"} => 0
+    -- if 0 < 1
+  (; \n ;)
+  | {"GB" "GC" "GD"} => 0
+  (; \n ;)
+  | {"GC" "GD"} => 0
+    -- if 0 < 1
+  (; \n ;)
+  | {"GD" "GE"} => 0
+    -- if 0 < 1
+    -- if 1 > 0
+  (; \n ;)
+  | {"GE" "GF"} => 0
+    -- if 0 < 1
+  (; \n ;)
+  | {"GFA" "GF"} => 0
+  | {"GFB" "GF"} => 1
+  | "GFC" => 2
+  (; \n ;)
+  | "GG" => 0
+    -- if 1 > 0
+  (; \n ;)
+  | "GH" => 0
+    -- if 1 > 0
+  (; \n ;)
+  | "GI" => {0 1 2}
+    -- if 0 < 1
+    -- if 1 > 0
+  (; \n ;)
+  | {"GJ" "GJ" "G" "J"} => 0
+  (; \n ;)
+  | {"GK" "GJ" "G" "J"} => 0
+    -- if 0 < 1
+    -- if 1 > 0
+  (; \n ;)
+  | "GI" => {0 1 2}
+    ----
+    -- if 0 < 1
+    -- if 1 > 0
+  (; \n ;)
+  | "GI" => {0 1 2}
+    ----
+    -- if 0 < 1
+    -- if 1 > 0
+
+
+
+def $func(nat : nat, nat : nat) : nat*
+def $func(n, m) = 0
+def $func(n, m) = 0
+  -- if n < m
+def $func(n, m) = 0
+  -- if n > m
+  -- if m < n
+def $func(n, m) = {0 1}
+  -- if n < m
+  -- if m > n
+def $func(n, m) = {0 1}
+  -- if n < m
+  -- if m > n
+def $func(n, m) = {0 1 2}
+  -- if n < m
+  -- if m > n
+def $func(n, m) = {0 1 2}
+  -- if n < m
+  -- if m > n
+def $func(n, m) = {0 1 2}
+  -- if n < m
+  -- if m > n
+
+
+
+relation Rel: {argh borg} -> {curb dork}
+rule Rel/A:
+  {argh borg} -> {curb dork}
+rule Rel/B:
+  {argh borg} -> {curb dork}
+  -- if 0 < 1
+rule Rel/C:
+  {argh borg} -> {curb dork}
+  -- if 0 < 1
+  -- if 1 > 0
+rule Rel/D:
+  {argh borg} -> {curb dork}
+  -- if 0 < 1
+  -- if 1 > 0
+rule Rel/E:
+  {argh borg} -> {curb dork}
+  -- if 0 < 1
+  -- if 1 > 0
+rule Rel/F:
+  {argh borg} -> {curb dork}
+  -- if 0 < 1
+  -- if 1 > 0
+rule Rel/G:
+  {argh borg} -> {curb dork}
+  -- if 0 < 1
+  -- if 1 > 0
+rule Rel/DD:
+  {argh borg} -> {curb dork}
+  -- if 0 < 1
+  -- if 1 > 0
+rule Rel/EE:
+  {argh borg} -> {curb dork}
+  -- if 0 < 1
+  -- if 1 > 0
+rule Rel/FF:
+  {argh borg} -> {curb dork}
+  -- if 0 < 1
+  -- if 1 > 0
+rule Rel/GG:
+  {argh borg} -> {curb dork}
+  -- if 0 < 1
+  -- if 1 > 0
+
+== Elaboration...
+== IL Validation...
+== Latex Generation...
+== Complete.
diff --git a/spectec/test-middlend/TEST.md b/spectec/test-middlend/TEST.md
index c86bb6dfa..f75b85ed8 100644
--- a/spectec/test-middlend/TEST.md
+++ b/spectec/test-middlend/TEST.md
@@ -8698,14 +8698,21 @@ grammar Btypesec : type*
   prod{`ty*` : type*} ty*{ty <- `ty*`}:Bsection_(1, syntax type, grammar Blist(syntax type, grammar Btype)) => ty*{ty <- `ty*`}
 
 ;; ../../../../specification/wasm-3.0/5.4-binary.modules.spectec
-grammar Bimport : import
+grammar Bimport : (name, externtype)
   ;; ../../../../specification/wasm-3.0/5.4-binary.modules.spectec
-  prod{nm_1 : name, nm_2 : name, xt : externtype} {{nm_1:Bname} {nm_2:Bname} {xt:Bexterntype}} => IMPORT_import(nm_1, nm_2, xt)
+  prod{nm_2 : name, xt : externtype} {{nm_2:Bname} {xt:Bexterntype}} => (nm_2, xt)
+
+;; ../../../../specification/wasm-3.0/5.4-binary.modules.spectec
+grammar Bimports : import*
+  ;; ../../../../specification/wasm-3.0/5.4-binary.modules.spectec
+  prod{nm_1 : name, nm_2 : name, xt : externtype} {{nm_1:Bname} {(nm_2, xt):Bimport}} => [IMPORT_import(nm_1, nm_2, xt)]
+  ;; ../../../../specification/wasm-3.0/5.4-binary.modules.spectec
+  prod{nm_1 : name, `nm_2*` : name*, `xt*` : externtype*} {{0x01} {0xFF} {nm_1:Bname} {(nm_2, xt)*{nm_2 <- `nm_2*`, xt <- `xt*`}:Blist(syntax (name, externtype), grammar Bimport)}} => IMPORT_import(nm_1, nm_2, xt)*{nm_2 <- `nm_2*`, xt <- `xt*`}
 
 ;; ../../../../specification/wasm-3.0/5.4-binary.modules.spectec
 grammar Bimportsec : import*
   ;; ../../../../specification/wasm-3.0/5.4-binary.modules.spectec
-  prod{`im*` : import*} im*{im <- `im*`}:Bsection_(2, syntax import, grammar Blist(syntax import, grammar Bimport)) => im*{im <- `im*`}
+  prod{`im**` : import**} im*{im <- `im*`}*{`im*` <- `im**`}:Bsection_(2, syntax import*, grammar Blist(syntax import*, grammar Bimports)) => $concat_(syntax import, im*{im <- `im*`}*{`im*` <- `im**`})
 
 ;; ../../../../specification/wasm-3.0/5.4-binary.modules.spectec
 grammar Bfuncsec : typeidx*
@@ -10853,6 +10860,9 @@ grammar Tstart_(I : I) : (start, idctxt)
   ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
   prod{x : idx} {{"("} {"start"} {x:Tfuncidx_(I)} {")"}} => (START_start(x), {TYPES [], TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [], DATAS [], ELEMS [], LOCALS [], LABELS [], FIELDS [], TYPEDEFS []})
 
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
+grammar Timports_(I : I) : (import*, idctxt)
+
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 grammar Timport_(I : I) : (import, idctxt)
   ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
@@ -10953,13 +10963,13 @@ syntax decl =
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:258.1-258.76
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:261.1-261.76
 def $typesd(decl*) : type*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:270.1-270.23
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:273.1-273.23
   def $typesd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:271.1-271.48
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:274.1-274.48
   def $typesd{type : type, `decl'*` : decl*}([(type : type <: decl)] ++ decl'*{decl' <- `decl'*`}) = [type] ++ $typesd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:272.1-272.57
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:275.1-275.57
   def $typesd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $typesd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -10967,13 +10977,13 @@ def $typesd(decl*) : type*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:259.1-259.78
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:262.1-262.78
 def $importsd(decl*) : import*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:274.1-274.25
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:277.1-277.25
   def $importsd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:275.1-275.56
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:278.1-278.56
   def $importsd{import : import, `decl'*` : decl*}([(import : import <: decl)] ++ decl'*{decl' <- `decl'*`}) = [import] ++ $importsd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:276.1-276.61
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:279.1-279.61
   def $importsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $importsd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -10981,13 +10991,13 @@ def $importsd(decl*) : import*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:260.1-260.75
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:263.1-263.75
 def $tagsd(decl*) : tag*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:278.1-278.22
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:281.1-281.22
   def $tagsd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:279.1-279.44
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:282.1-282.44
   def $tagsd{tag : tag, `decl'*` : decl*}([(tag : tag <: decl)] ++ decl'*{decl' <- `decl'*`}) = [tag] ++ $tagsd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:280.1-280.55
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:283.1-283.55
   def $tagsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $tagsd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -10995,13 +11005,13 @@ def $tagsd(decl*) : tag*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:261.1-261.78
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:264.1-264.78
 def $globalsd(decl*) : global*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:282.1-282.25
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:285.1-285.25
   def $globalsd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:283.1-283.56
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:286.1-286.56
   def $globalsd{global : global, `decl'*` : decl*}([(global : global <: decl)] ++ decl'*{decl' <- `decl'*`}) = [global] ++ $globalsd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:284.1-284.61
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:287.1-287.61
   def $globalsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $globalsd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -11009,13 +11019,13 @@ def $globalsd(decl*) : global*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:262.1-262.75
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:265.1-265.75
 def $memsd(decl*) : mem*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:286.1-286.22
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:289.1-289.22
   def $memsd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:287.1-287.44
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:290.1-290.44
   def $memsd{mem : mem, `decl'*` : decl*}([(mem : mem <: decl)] ++ decl'*{decl' <- `decl'*`}) = [mem] ++ $memsd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:288.1-288.55
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:291.1-291.55
   def $memsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $memsd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -11023,13 +11033,13 @@ def $memsd(decl*) : mem*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:263.1-263.77
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:266.1-266.77
 def $tablesd(decl*) : table*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:290.1-290.24
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:293.1-293.24
   def $tablesd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:291.1-291.52
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:294.1-294.52
   def $tablesd{table : table, `decl'*` : decl*}([(table : table <: decl)] ++ decl'*{decl' <- `decl'*`}) = [table] ++ $tablesd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:292.1-292.59
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:295.1-295.59
   def $tablesd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $tablesd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -11037,13 +11047,13 @@ def $tablesd(decl*) : table*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:264.1-264.76
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:267.1-267.76
 def $funcsd(decl*) : func*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:294.1-294.23
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:297.1-297.23
   def $funcsd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:295.1-295.48
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:298.1-298.48
   def $funcsd{func : func, `decl'*` : decl*}([(func : func <: decl)] ++ decl'*{decl' <- `decl'*`}) = [func] ++ $funcsd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:296.1-296.57
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:299.1-299.57
   def $funcsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $funcsd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -11051,13 +11061,13 @@ def $funcsd(decl*) : func*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:265.1-265.76
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:268.1-268.76
 def $datasd(decl*) : data*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:298.1-298.23
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:301.1-301.23
   def $datasd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:299.1-299.48
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:302.1-302.48
   def $datasd{data : data, `decl'*` : decl*}([(data : data <: decl)] ++ decl'*{decl' <- `decl'*`}) = [data] ++ $datasd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:300.1-300.57
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:303.1-303.57
   def $datasd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $datasd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -11065,13 +11075,13 @@ def $datasd(decl*) : data*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:266.1-266.76
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:269.1-269.76
 def $elemsd(decl*) : elem*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:302.1-302.23
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:305.1-305.23
   def $elemsd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:303.1-303.48
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:306.1-306.48
   def $elemsd{elem : elem, `decl'*` : decl*}([(elem : elem <: decl)] ++ decl'*{decl' <- `decl'*`}) = [elem] ++ $elemsd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:304.1-304.57
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:307.1-307.57
   def $elemsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $elemsd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -11079,13 +11089,13 @@ def $elemsd(decl*) : elem*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:267.1-267.77
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:270.1-270.77
 def $startsd(decl*) : start*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:306.1-306.24
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:309.1-309.24
   def $startsd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:307.1-307.52
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:310.1-310.52
   def $startsd{start : start, `decl'*` : decl*}([(start : start <: decl)] ++ decl'*{decl' <- `decl'*`}) = [start] ++ $startsd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:308.1-308.59
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:311.1-311.59
   def $startsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $startsd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -11093,13 +11103,13 @@ def $startsd(decl*) : start*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:268.1-268.78
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:271.1-271.78
 def $exportsd(decl*) : export*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:310.1-310.25
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:313.1-313.25
   def $exportsd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:311.1-311.56
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:314.1-314.56
   def $exportsd{export : export, `decl'*` : decl*}([(export : export <: decl)] ++ decl'*{decl' <- `decl'*`}) = [export] ++ $exportsd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:312.1-312.61
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:315.1-315.61
   def $exportsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $exportsd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -20039,14 +20049,21 @@ grammar Btypesec : type*
   prod{`ty*` : type*} ty*{ty <- `ty*`}:Bsection_(1, syntax type, grammar Blist(syntax type, grammar Btype)) => ty*{ty <- `ty*`}
 
 ;; ../../../../specification/wasm-3.0/5.4-binary.modules.spectec
-grammar Bimport : import
+grammar Bimport : (name, externtype)
+  ;; ../../../../specification/wasm-3.0/5.4-binary.modules.spectec
+  prod{nm_2 : name, xt : externtype} {{nm_2:Bname} {xt:Bexterntype}} => (nm_2, xt)
+
+;; ../../../../specification/wasm-3.0/5.4-binary.modules.spectec
+grammar Bimports : import*
   ;; ../../../../specification/wasm-3.0/5.4-binary.modules.spectec
-  prod{nm_1 : name, nm_2 : name, xt : externtype} {{nm_1:Bname} {nm_2:Bname} {xt:Bexterntype}} => IMPORT_import(nm_1, nm_2, xt)
+  prod{nm_1 : name, nm_2 : name, xt : externtype} {{nm_1:Bname} {(nm_2, xt):Bimport}} => [IMPORT_import(nm_1, nm_2, xt)]
+  ;; ../../../../specification/wasm-3.0/5.4-binary.modules.spectec
+  prod{nm_1 : name, `nm_2*` : name*, `xt*` : externtype*} {{0x01} {0xFF} {nm_1:Bname} {(nm_2, xt)*{nm_2 <- `nm_2*`, xt <- `xt*`}:Blist(syntax (name, externtype), grammar Bimport)}} => IMPORT_import(nm_1, nm_2, xt)*{nm_2 <- `nm_2*`, xt <- `xt*`}
 
 ;; ../../../../specification/wasm-3.0/5.4-binary.modules.spectec
 grammar Bimportsec : import*
   ;; ../../../../specification/wasm-3.0/5.4-binary.modules.spectec
-  prod{`im*` : import*} im*{im <- `im*`}:Bsection_(2, syntax import, grammar Blist(syntax import, grammar Bimport)) => im*{im <- `im*`}
+  prod{`im**` : import**} im*{im <- `im*`}*{`im*` <- `im**`}:Bsection_(2, syntax import*, grammar Blist(syntax import*, grammar Bimports)) => $concat_(syntax import, im*{im <- `im*`}*{`im*` <- `im**`})
 
 ;; ../../../../specification/wasm-3.0/5.4-binary.modules.spectec
 grammar Bfuncsec : typeidx*
@@ -22194,6 +22211,9 @@ grammar Tstart_(I : I) : (start, idctxt)
   ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
   prod{x : idx} {{"("} {"start"} {x:Tfuncidx_(I)} {")"}} => (START_start(x), {TYPES [], TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [], DATAS [], ELEMS [], LOCALS [], LABELS [], FIELDS [], TYPEDEFS []})
 
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
+grammar Timports_(I : I) : (import*, idctxt)
+
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 grammar Timport_(I : I) : (import, idctxt)
   ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
@@ -22294,13 +22314,13 @@ syntax decl =
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:258.1-258.76
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:261.1-261.76
 def $typesd(decl*) : type*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:270.1-270.23
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:273.1-273.23
   def $typesd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:271.1-271.48
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:274.1-274.48
   def $typesd{type : type, `decl'*` : decl*}([(type : type <: decl)] ++ decl'*{decl' <- `decl'*`}) = [type] ++ $typesd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:272.1-272.57
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:275.1-275.57
   def $typesd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $typesd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -22308,13 +22328,13 @@ def $typesd(decl*) : type*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:259.1-259.78
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:262.1-262.78
 def $importsd(decl*) : import*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:274.1-274.25
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:277.1-277.25
   def $importsd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:275.1-275.56
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:278.1-278.56
   def $importsd{import : import, `decl'*` : decl*}([(import : import <: decl)] ++ decl'*{decl' <- `decl'*`}) = [import] ++ $importsd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:276.1-276.61
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:279.1-279.61
   def $importsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $importsd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -22322,13 +22342,13 @@ def $importsd(decl*) : import*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:260.1-260.75
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:263.1-263.75
 def $tagsd(decl*) : tag*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:278.1-278.22
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:281.1-281.22
   def $tagsd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:279.1-279.44
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:282.1-282.44
   def $tagsd{tag : tag, `decl'*` : decl*}([(tag : tag <: decl)] ++ decl'*{decl' <- `decl'*`}) = [tag] ++ $tagsd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:280.1-280.55
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:283.1-283.55
   def $tagsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $tagsd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -22336,13 +22356,13 @@ def $tagsd(decl*) : tag*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:261.1-261.78
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:264.1-264.78
 def $globalsd(decl*) : global*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:282.1-282.25
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:285.1-285.25
   def $globalsd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:283.1-283.56
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:286.1-286.56
   def $globalsd{global : global, `decl'*` : decl*}([(global : global <: decl)] ++ decl'*{decl' <- `decl'*`}) = [global] ++ $globalsd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:284.1-284.61
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:287.1-287.61
   def $globalsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $globalsd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -22350,13 +22370,13 @@ def $globalsd(decl*) : global*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:262.1-262.75
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:265.1-265.75
 def $memsd(decl*) : mem*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:286.1-286.22
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:289.1-289.22
   def $memsd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:287.1-287.44
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:290.1-290.44
   def $memsd{mem : mem, `decl'*` : decl*}([(mem : mem <: decl)] ++ decl'*{decl' <- `decl'*`}) = [mem] ++ $memsd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:288.1-288.55
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:291.1-291.55
   def $memsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $memsd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -22364,13 +22384,13 @@ def $memsd(decl*) : mem*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:263.1-263.77
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:266.1-266.77
 def $tablesd(decl*) : table*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:290.1-290.24
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:293.1-293.24
   def $tablesd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:291.1-291.52
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:294.1-294.52
   def $tablesd{table : table, `decl'*` : decl*}([(table : table <: decl)] ++ decl'*{decl' <- `decl'*`}) = [table] ++ $tablesd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:292.1-292.59
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:295.1-295.59
   def $tablesd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $tablesd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -22378,13 +22398,13 @@ def $tablesd(decl*) : table*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:264.1-264.76
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:267.1-267.76
 def $funcsd(decl*) : func*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:294.1-294.23
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:297.1-297.23
   def $funcsd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:295.1-295.48
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:298.1-298.48
   def $funcsd{func : func, `decl'*` : decl*}([(func : func <: decl)] ++ decl'*{decl' <- `decl'*`}) = [func] ++ $funcsd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:296.1-296.57
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:299.1-299.57
   def $funcsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $funcsd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -22392,13 +22412,13 @@ def $funcsd(decl*) : func*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:265.1-265.76
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:268.1-268.76
 def $datasd(decl*) : data*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:298.1-298.23
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:301.1-301.23
   def $datasd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:299.1-299.48
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:302.1-302.48
   def $datasd{data : data, `decl'*` : decl*}([(data : data <: decl)] ++ decl'*{decl' <- `decl'*`}) = [data] ++ $datasd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:300.1-300.57
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:303.1-303.57
   def $datasd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $datasd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -22406,13 +22426,13 @@ def $datasd(decl*) : data*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:266.1-266.76
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:269.1-269.76
 def $elemsd(decl*) : elem*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:302.1-302.23
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:305.1-305.23
   def $elemsd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:303.1-303.48
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:306.1-306.48
   def $elemsd{elem : elem, `decl'*` : decl*}([(elem : elem <: decl)] ++ decl'*{decl' <- `decl'*`}) = [elem] ++ $elemsd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:304.1-304.57
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:307.1-307.57
   def $elemsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $elemsd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -22420,13 +22440,13 @@ def $elemsd(decl*) : elem*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:267.1-267.77
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:270.1-270.77
 def $startsd(decl*) : start*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:306.1-306.24
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:309.1-309.24
   def $startsd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:307.1-307.52
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:310.1-310.52
   def $startsd{start : start, `decl'*` : decl*}([(start : start <: decl)] ++ decl'*{decl' <- `decl'*`}) = [start] ++ $startsd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:308.1-308.59
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:311.1-311.59
   def $startsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $startsd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -22434,13 +22454,13 @@ def $startsd(decl*) : start*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:268.1-268.78
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:271.1-271.78
 def $exportsd(decl*) : export*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:310.1-310.25
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:313.1-313.25
   def $exportsd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:311.1-311.56
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:314.1-314.56
   def $exportsd{export : export, `decl'*` : decl*}([(export : export <: decl)] ++ decl'*{decl' <- `decl'*`}) = [export] ++ $exportsd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:312.1-312.61
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:315.1-315.61
   def $exportsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $exportsd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -31559,14 +31579,21 @@ grammar Btypesec : type*
   prod{`ty*` : type*} ty*{ty <- `ty*`}:Bsection_(1, syntax type, grammar Blist(syntax type, grammar Btype)) => ty*{ty <- `ty*`}
 
 ;; ../../../../specification/wasm-3.0/5.4-binary.modules.spectec
-grammar Bimport : import
+grammar Bimport : (name, externtype)
   ;; ../../../../specification/wasm-3.0/5.4-binary.modules.spectec
-  prod{nm_1 : name, nm_2 : name, xt : externtype} {{nm_1:Bname} {nm_2:Bname} {xt:Bexterntype}} => IMPORT_import(nm_1, nm_2, xt)
+  prod{nm_2 : name, xt : externtype} {{nm_2:Bname} {xt:Bexterntype}} => (nm_2, xt)
+
+;; ../../../../specification/wasm-3.0/5.4-binary.modules.spectec
+grammar Bimports : import*
+  ;; ../../../../specification/wasm-3.0/5.4-binary.modules.spectec
+  prod{nm_1 : name, nm_2 : name, xt : externtype} {{nm_1:Bname} {(nm_2, xt):Bimport}} => [IMPORT_import(nm_1, nm_2, xt)]
+  ;; ../../../../specification/wasm-3.0/5.4-binary.modules.spectec
+  prod{nm_1 : name, `nm_2*` : name*, `xt*` : externtype*} {{0x01} {0xFF} {nm_1:Bname} {(nm_2, xt)*{nm_2 <- `nm_2*`, xt <- `xt*`}:Blist(syntax (name, externtype), grammar Bimport)}} => IMPORT_import(nm_1, nm_2, xt)*{nm_2 <- `nm_2*`, xt <- `xt*`}
 
 ;; ../../../../specification/wasm-3.0/5.4-binary.modules.spectec
 grammar Bimportsec : import*
   ;; ../../../../specification/wasm-3.0/5.4-binary.modules.spectec
-  prod{`im*` : import*} im*{im <- `im*`}:Bsection_(2, syntax import, grammar Blist(syntax import, grammar Bimport)) => im*{im <- `im*`}
+  prod{`im**` : import**} im*{im <- `im*`}*{`im*` <- `im**`}:Bsection_(2, syntax import*, grammar Blist(syntax import*, grammar Bimports)) => $concat_(syntax import, im*{im <- `im*`}*{`im*` <- `im**`})
 
 ;; ../../../../specification/wasm-3.0/5.4-binary.modules.spectec
 grammar Bfuncsec : typeidx*
@@ -33714,6 +33741,9 @@ grammar Tstart_(I : I) : (start, idctxt)
   ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
   prod{x : idx} {{"("} {"start"} {x:Tfuncidx_(I)} {")"}} => (START_start(x), {TYPES [], TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [], DATAS [], ELEMS [], LOCALS [], LABELS [], FIELDS [], TYPEDEFS []})
 
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
+grammar Timports_(I : I) : (import*, idctxt)
+
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 grammar Timport_(I : I) : (import, idctxt)
   ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
@@ -33814,13 +33844,13 @@ syntax decl =
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:258.1-258.76
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:261.1-261.76
 def $typesd(decl*) : type*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:270.1-270.23
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:273.1-273.23
   def $typesd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:271.1-271.48
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:274.1-274.48
   def $typesd{type : type, `decl'*` : decl*}([(type : type <: decl)] ++ decl'*{decl' <- `decl'*`}) = [type] ++ $typesd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:272.1-272.57
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:275.1-275.57
   def $typesd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $typesd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -33828,13 +33858,13 @@ def $typesd(decl*) : type*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:259.1-259.78
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:262.1-262.78
 def $importsd(decl*) : import*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:274.1-274.25
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:277.1-277.25
   def $importsd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:275.1-275.56
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:278.1-278.56
   def $importsd{import : import, `decl'*` : decl*}([(import : import <: decl)] ++ decl'*{decl' <- `decl'*`}) = [import] ++ $importsd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:276.1-276.61
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:279.1-279.61
   def $importsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $importsd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -33842,13 +33872,13 @@ def $importsd(decl*) : import*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:260.1-260.75
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:263.1-263.75
 def $tagsd(decl*) : tag*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:278.1-278.22
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:281.1-281.22
   def $tagsd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:279.1-279.44
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:282.1-282.44
   def $tagsd{tag : tag, `decl'*` : decl*}([(tag : tag <: decl)] ++ decl'*{decl' <- `decl'*`}) = [tag] ++ $tagsd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:280.1-280.55
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:283.1-283.55
   def $tagsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $tagsd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -33856,13 +33886,13 @@ def $tagsd(decl*) : tag*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:261.1-261.78
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:264.1-264.78
 def $globalsd(decl*) : global*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:282.1-282.25
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:285.1-285.25
   def $globalsd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:283.1-283.56
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:286.1-286.56
   def $globalsd{global : global, `decl'*` : decl*}([(global : global <: decl)] ++ decl'*{decl' <- `decl'*`}) = [global] ++ $globalsd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:284.1-284.61
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:287.1-287.61
   def $globalsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $globalsd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -33870,13 +33900,13 @@ def $globalsd(decl*) : global*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:262.1-262.75
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:265.1-265.75
 def $memsd(decl*) : mem*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:286.1-286.22
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:289.1-289.22
   def $memsd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:287.1-287.44
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:290.1-290.44
   def $memsd{mem : mem, `decl'*` : decl*}([(mem : mem <: decl)] ++ decl'*{decl' <- `decl'*`}) = [mem] ++ $memsd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:288.1-288.55
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:291.1-291.55
   def $memsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $memsd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -33884,13 +33914,13 @@ def $memsd(decl*) : mem*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:263.1-263.77
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:266.1-266.77
 def $tablesd(decl*) : table*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:290.1-290.24
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:293.1-293.24
   def $tablesd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:291.1-291.52
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:294.1-294.52
   def $tablesd{table : table, `decl'*` : decl*}([(table : table <: decl)] ++ decl'*{decl' <- `decl'*`}) = [table] ++ $tablesd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:292.1-292.59
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:295.1-295.59
   def $tablesd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $tablesd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -33898,13 +33928,13 @@ def $tablesd(decl*) : table*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:264.1-264.76
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:267.1-267.76
 def $funcsd(decl*) : func*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:294.1-294.23
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:297.1-297.23
   def $funcsd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:295.1-295.48
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:298.1-298.48
   def $funcsd{func : func, `decl'*` : decl*}([(func : func <: decl)] ++ decl'*{decl' <- `decl'*`}) = [func] ++ $funcsd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:296.1-296.57
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:299.1-299.57
   def $funcsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $funcsd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -33912,13 +33942,13 @@ def $funcsd(decl*) : func*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:265.1-265.76
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:268.1-268.76
 def $datasd(decl*) : data*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:298.1-298.23
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:301.1-301.23
   def $datasd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:299.1-299.48
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:302.1-302.48
   def $datasd{data : data, `decl'*` : decl*}([(data : data <: decl)] ++ decl'*{decl' <- `decl'*`}) = [data] ++ $datasd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:300.1-300.57
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:303.1-303.57
   def $datasd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $datasd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -33926,13 +33956,13 @@ def $datasd(decl*) : data*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:266.1-266.76
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:269.1-269.76
 def $elemsd(decl*) : elem*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:302.1-302.23
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:305.1-305.23
   def $elemsd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:303.1-303.48
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:306.1-306.48
   def $elemsd{elem : elem, `decl'*` : decl*}([(elem : elem <: decl)] ++ decl'*{decl' <- `decl'*`}) = [elem] ++ $elemsd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:304.1-304.57
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:307.1-307.57
   def $elemsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $elemsd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -33940,13 +33970,13 @@ def $elemsd(decl*) : elem*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:267.1-267.77
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:270.1-270.77
 def $startsd(decl*) : start*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:306.1-306.24
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:309.1-309.24
   def $startsd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:307.1-307.52
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:310.1-310.52
   def $startsd{start : start, `decl'*` : decl*}([(start : start <: decl)] ++ decl'*{decl' <- `decl'*`}) = [start] ++ $startsd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:308.1-308.59
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:311.1-311.59
   def $startsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $startsd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -33954,13 +33984,13 @@ def $startsd(decl*) : start*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:268.1-268.78
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:271.1-271.78
 def $exportsd(decl*) : export*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:310.1-310.25
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:313.1-313.25
   def $exportsd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:311.1-311.56
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:314.1-314.56
   def $exportsd{export : export, `decl'*` : decl*}([(export : export <: decl)] ++ decl'*{decl' <- `decl'*`}) = [export] ++ $exportsd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:312.1-312.61
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:315.1-315.61
   def $exportsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $exportsd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
diff --git a/spectec/test-splice/TEST.md b/spectec/test-splice/TEST.md
index 8b4853429..db9142492 100644
--- a/spectec/test-splice/TEST.md
+++ b/spectec/test-splice/TEST.md
@@ -546,6 +546,7 @@ warning: grammar `Bglobaltype` was never spliced
 warning: grammar `Bheaptype` was never spliced
 warning: grammar `BiN` was never spliced
 warning: grammar `Bimport` was never spliced
+warning: grammar `Bimports` was never spliced
 warning: grammar `Bimportsec` was never spliced
 warning: grammar `Binstr/parametric` was never spliced
 warning: grammar `Binstr/block` was never spliced
@@ -768,6 +769,7 @@ warning: grammar `Timport_/abbrev-mem` was never spliced
 warning: grammar `Timport_/abbrev-table` was never spliced
 warning: grammar `Timport_/abbrev-func` was never spliced
 warning: grammar `Timportdots` was never spliced
+warning: grammar `Timports_/abbrev` was never spliced
 warning: grammar `Tinstr_` was never spliced
 warning: grammar `Tinstrs_/unfolded` was never spliced
 warning: grammar `Tinstrs_/folded` was never spliced