From 6af6fb6b2a50e4066685d82e16bbd613ea7b15ba Mon Sep 17 00:00:00 2001
From: Benjamin Lipp <blipp@rosenpass.eu>
Date: Tue, 25 Nov 2025 16:00:16 +0100
Subject: [PATCH] fix: pterm can resolve to NAT

---
 marzipan/src/parser.py | 1 +
 1 file changed, 1 insertion(+)

diff --git a/marzipan/src/parser.py b/marzipan/src/parser.py
index ef1324e..d899fb2 100644
--- a/marzipan/src/parser.py
+++ b/marzipan/src/parser.py
@@ -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