Parser: fix #3530

FStarLang · Oct 6, 2024 · 31ab322 · 31ab322
1 parent 0bf49cb
commit 31ab322
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/ocaml/fstar-lib/FStar_Parser_Parse.mly b/ocaml/fstar-lib/FStar_Parser_Parse.mly
@@ -1238,10 +1238,11 @@ simpleArrowDomain:
   | LBRACE_BAR t=tmEqNoRefinement BAR_RBRACE { ((Some TypeClassArg, []), t) }
   | aq_opt=ioption(aqual) attrs_opt=ioption(binderAttributes) dom_tm=tmEqNoRefinement { (aq_opt, none_to_empty_list attrs_opt), dom_tm }
 
-(* Tm already account for ( term ), we need to add an explicit case for (#Tm) *)
+(* Tm already accounts for ( term ), we need to add an explicit case for (#Tm), (#[@@@...]Tm) and ([@@@...]Tm) *)
 %inline tmArrowDomain(Tm):
   | LBRACE_BAR t=Tm BAR_RBRACE { ((Some TypeClassArg, []), t) }
   | LPAREN q=aqual attrs_opt=ioption(binderAttributes) dom_tm=Tm RPAREN { (Some q, none_to_empty_list attrs_opt), dom_tm }
+  | LPAREN attrs=binderAttributes dom_tm=Tm RPAREN { (None, attrs), dom_tm }
   | aq_opt=ioption(aqual) attrs_opt=ioption(binderAttributes) dom_tm=Tm { (aq_opt, none_to_empty_list attrs_opt), dom_tm }
 
 tmFormula: