Do not require parens in assert/assume.

FStarLang · Aug 19, 2024 · fcc1b9c · fcc1b9c
1 parent 88a7338
commit fcc1b9c
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 3 deletions.
diff --git a/ocaml/fstar-lib/FStar_Parser_Parse.mly b/ocaml/fstar-lib/FStar_Parser_Parse.mly
@@ -1009,12 +1009,12 @@ noSeqTerm:
         let branches = focusBranches pbs (rr2 $loc($1) $loc(pbs)) in
         mk_function branches (rr $loc) (rr2 $loc($1) $loc(pbs))
       }
-  | a=ASSUME e=atomicTerm
+  | a=ASSUME e=noSeqTerm
       { let a = set_lid_range assume_lid (rr $loc(a)) in
         mkExplicitApp (mk_term (Var a) (rr $loc(a)) Expr) [e] (rr $loc)
       }
 
-  | a=ASSERT e=atomicTerm tactic_opt=option(BY tactic=thunk2(typ) {tactic})
+  | a=ASSERT e=noSeqTerm tactic_opt=option(BY tactic=thunk2(typ) {tactic})
       {
         match tactic_opt with
         | None ->

diff --git a/tests/bug-reports/Parentheses.fst b/tests/bug-reports/Parentheses.fst
@@ -9,4 +9,12 @@ let trailing_fun_does_not_require_parens :
 
 let trailing_fun_swallows_seqs :
     squash (forall (x: nat) (y: nat). x + y >= 0) =
-  forall_intro fun x -> forall_intro fun y -> (); ()
+  forall_intro fun x -> forall_intro fun y -> (); ()
+
+let assert_does_not_require_parens : unit =
+  assert 8 < 42;
+  ()
+
+let assume_does_not_require_parens : False =
+  assume 0 == 1;
+  ()