Add a test for FStarLang#3530

mtzguido · Oct 6, 2024 · 971eb6d · 971eb6d
1 parent 31ab322
commit 971eb6d
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 1 deletion.
diff --git a/tests/bug-reports/Bug3530.fst b/tests/bug-reports/Bug3530.fst
@@ -0,0 +1,11 @@
+module Bug3530
+
+let _ = x:int -> bool
+let _ = #x:int -> bool
+let _ = #[@@@1]x:int -> bool
+let _ = [@@@1]x:int -> bool
+
+let _ = (x:int) -> bool
+let _ = (#x:int) -> bool
+let _ = (#[@@@1]x:int) -> bool
+let _ = ([@@@1]x:int) -> bool
diff --git a/tests/bug-reports/Makefile b/tests/bug-reports/Makefile
@@ -80,7 +80,7 @@ SHOULD_VERIFY_CLOSED=\
 	Bug2155.fst Bug3224a.fst Bug3224b.fst Bug3236.fst Bug3252.fst \
 	BugBoxInjectivity.fst BugTypeParamProjector.fst Bug2172.fst Bug3266.fst		\
 	Bug3264a.fst Bug3264b.fst Bug3286a.fst Bug3286b.fst Bug3320.fst Bug2583.fst \
-	Bug2419.fst Bug3353.fst Bug3426.fst
+	Bug2419.fst Bug3353.fst Bug3426.fst Bug3530.fst
 
 
 SHOULD_VERIFY_INTERFACE_CLOSED=Bug771.fsti Bug771b.fsti