Add test for #1562

GaloisInc · Aug 10, 2023 · fbfad1f · fbfad1f
1 parent bcb60f2
commit fbfad1f
Show file tree

Hide file tree

Showing 3 changed files with 17 additions and 0 deletions.
diff --git a/tests/issues/issue1562.cry b/tests/issues/issue1562.cry
@@ -0,0 +1,13 @@
+interface submodule I where
+  type Zp = [8]
+
+submodule F where
+  import interface submodule I
+
+submodule M where
+  // this is unused, but just here because syntactically we cannot have an empty
+  // module
+  type Empty = Bit
+
+submodule F1 = submodule F { submodule M }
+submodule F2 = submodule F { submodule M }
diff --git a/tests/issues/issue1562.icry b/tests/issues/issue1562.icry
@@ -0,0 +1 @@
+:l issue1562.cry
diff --git a/tests/issues/issue1562.icry.stdout b/tests/issues/issue1562.icry.stdout
@@ -0,0 +1,3 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Main