Add repro for FStarLang#169

mtzguido · Feb 7, 2025 · ad8d11d · ad8d11d
1 parent 1730c03
commit ad8d11d
Show file tree

Hide file tree

Showing 2 changed files with 21 additions and 0 deletions.
diff --git a/test/bug-reports/Bug169.fst b/test/bug-reports/Bug169.fst
@@ -0,0 +1,15 @@
+module Bug169
+
+#lang-pulse
+open Pulse
+
+// - Failed to desugar pulse extension text
+let is_sublist (a b : Seq.seq nat) : prop = true
+
+[@@expect_failure [72]]
+fn check_is_sublist (m: SiveT.t)
+  requires emp
+  ensures emp
+{
+  ()
+}
diff --git a/test/bug-reports/Bug169.fst.output.expected b/test/bug-reports/Bug169.fst.output.expected
@@ -0,0 +1,6 @@
+>> Got issues: [
+* Error 72 at Bug169.fst(10,30-10,31):
+  - Identifier not found: [SiveT.t]
+  - Could not resolve module name SiveT
+
+>>]