Do not require parens for trailing fun.

FStarLang · Aug 15, 2024 · 375e6fd · 375e6fd
1 parent d33938a
commit 375e6fd
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 2 deletions.
diff --git a/ocaml/fstar-lib/FStar_Parser_Parse.mly b/ocaml/fstar-lib/FStar_Parser_Parse.mly
@@ -1167,8 +1167,6 @@ conjunctivePat:
 
 simpleTerm:
   | e=tmIff { e }
-  | FUN pats=nonempty_list(patternOrMultibinder) RARROW e=term
-      { mk_term (Abs(flatten pats, e)) (rr2 $loc($1) $loc(e)) Un }
 
 maybeFocusArrow:
   | RARROW          { false }
@@ -1420,6 +1418,8 @@ atomicTerm:
     { x }
   | x=opPrefixTerm(atomicTermQUident)
     { x }
+  | FUN pats=nonempty_list(patternOrMultibinder) RARROW e=term
+      { mk_term (Abs(flatten pats, e)) (rr2 $loc($1) $loc(e)) Un }
 
 atomicTermQUident:
   | id=quident

diff --git a/tests/bug-reports/Parentheses.fst b/tests/bug-reports/Parentheses.fst
@@ -0,0 +1,12 @@
+module Parentheses
+
+let forall_intro #t (#p: t->Type0) (h: (x:t -> squash (p x))) : squash (forall x. p x) =
+  Classical.Sugar.forall_intro _ _ h
+
+let trailing_fun_does_not_require_parens :
+    squash (forall (x: nat) (y: nat). x + y >= 0) =
+  forall_intro fun x -> forall_intro fun y -> ()
+
+let trailing_fun_swallows_seqs :
+    squash (forall (x: nat) (y: nat). x + y >= 0) =
+  forall_intro fun x -> forall_intro fun y -> (); ()