fix: pterm can resolve to NAT

This commit is contained in:
Benjamin Lipp
2025-11-25 16:00:16 +01:00
parent e3b43a59bf
commit 6af6fb6b2a

View File

@@ -208,6 +208,7 @@ proverif_grammar = Lark(
| "inductionOn" "=" "{" _non_empty_seq{IDENT} "}"
pterm: IDENT
| NAT
| "(" _maybe_empty_seq{pterm} ")"
| IDENT "(" _maybe_empty_seq{pterm} ")"
| choice_pterm