Skip to content

Commit

Permalink
parser: publish more symbols for Pulse
Browse files Browse the repository at this point in the history
  • Loading branch information
mtzguido committed Sep 5, 2024
1 parent c3311e1 commit 13e3913
Showing 1 changed file with 3 additions and 0 deletions.
3 changes: 3 additions & 0 deletions ocaml/fstar-lib/FStar_Parser_Parse.mly
Original file line number Diff line number Diff line change
Expand Up @@ -810,6 +810,7 @@ multiBinder:

| b=binder { [b] }

%public
binders: bss=list(bs=multiBinder {bs}) { flatten bss }

aqualifiedWithAttrs(X):
Expand Down Expand Up @@ -1144,6 +1145,7 @@ calcStep:
typ:
| t=simpleTerm { t }

%public
%inline quantifier:
| FORALL { fun x -> QForall x }
| EXISTS { fun x -> QExists x}
Expand All @@ -1158,6 +1160,7 @@ typ:
fun (x,y,z) -> QuantOp (op, x, y, z)
}

%public
trigger:
| { [] }
| LBRACE_COLON_PATTERN pats=disjunctivePats RBRACE { pats }
Expand Down

0 comments on commit 13e3913

Please sign in to comment.