From 5c463dcff3939aacdbfc5a923af5bdf15b3719cc Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Tue, 30 Apr 2024 14:24:37 +0200
Subject: [PATCH] update bnf

---
 doc/lambdapi.bnf | 29 ++++++++++++++++-------------
 1 file changed, 16 insertions(+), 13 deletions(-)

diff --git a/doc/lambdapi.bnf b/doc/lambdapi.bnf
index 75302a25a..3f794d123 100644
--- a/doc/lambdapi.bnf
+++ b/doc/lambdapi.bnf
@@ -18,22 +18,22 @@ QID ::= [UID "."]+ UID
 
 <search_query_alone> ::= <search_query> EOF
 
-<command> ::= "opaque" <qid_or_nat> ";"
+<command> ::= "opaque" <qid_or_int> ";"
             | "require" "open" <path>* ";"
             | "require" <path>* ";"
             | "require" <path> "as" <uid> ";"
             | "open" <path>* ";"
-            | <modifier>* "symbol" <uid_or_nat> <param_list>* ":" <term>
+            | <modifier>* "symbol" <uid_or_int> <param_list>* ":" <term>
               [<proof>] ";"
-            | <modifier>* "symbol" <uid_or_nat> <param_list>* [":" <term>]
+            | <modifier>* "symbol" <uid_or_int> <param_list>* [":" <term>]
               "≔" <term_proof> ";"
             | [<exposition>] <param_list>* "inductive" <inductive> ("with"
               <inductive>)* ";"
             | "rule" <rule> ("with" <rule>)* ";"
-            | "builtin" <stringlit> "≔" <qid_or_nat> ";"
+            | "builtin" <stringlit> "≔" <qid_or_int> ";"
             | "coerce_rule" <rule> ";"
             | "unif_rule" <unif_rule> ";"
-            | "notation" <qid_or_nat> <notation> ";"
+            | "notation" <qid_or_int> <notation> ";"
             | <query> ";"
             
 
@@ -70,11 +70,11 @@ QID ::= [UID "."]+ UID
 
 <uid> ::= UID
 
-<uid_or_nat> ::= <uid>
-               | <nat>
+<uid_or_int> ::= <uid>
+               | <int>
 
-<qid_or_nat> ::= <qid>
-               | <nat>
+<qid_or_int> ::= <qid>
+               | <int>
 
 <param_list> ::= <param>
                | "(" <param>+ ":" <term> ")"
@@ -104,6 +104,7 @@ QID ::= [UID "."]+ UID
           | "(" <term> ")"
           | "[" <term> "]"
           | <nat>
+          | "-"<nat>
 
 <env> ::= "." "[" [<term> (";" <term>)*] "]"
 
@@ -150,7 +151,7 @@ QID ::= [UID "."]+ UID
            | "reflexivity"
            | "remove" <uid>+
            | "rewrite" [<side>] [<rw_patt_spec>] <term>
-           | "simplify" [<qid_or_nat>]
+           | "simplify" [<qid_or_int>]
            | "solve"
            | "symmetry"
            | "try" <tactic>
@@ -167,7 +168,7 @@ QID ::= [UID "."]+ UID
 <inductive> ::= <uid> <param_list>* ":" <term> "≔" ["|"] [<constructor>
                 ("|" <constructor>)*]
 
-<constructor> ::= <uid_or_nat> <param_list>* ":" <term>
+<constructor> ::= <uid_or_int> <param_list>* ":" <term>
 
 <rule> ::= <term> "↪" <term>
 
@@ -182,8 +183,10 @@ QID ::= [UID "."]+ UID
              | "quantifier"
 
 <float_or_int> ::= <float>
-                 | "-"<nat>
-                 | <nat>
+                 | <int>
+
+<int> ::= "-"<nat>
+        | <nat>
 
 <maybe_generalize> ::= ["generalize"]