From c404faf0899e42b89e1fbc8b5e1da7f6b311882c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Fri, 24 Jan 2025 21:32:13 +0100
Subject: [PATCH 1/9] extend decimal notation to integers

---
 CHANGES.md                     |  4 ++-
 doc/commands.rst               | 15 ++++++++----
 doc/terms.rst                  |  6 ++---
 src/handle/query.ml            |  9 ++++---
 src/parsing/lpLexer.ml         | 13 ++++------
 src/parsing/lpParser.mly       | 39 +++++++++--------------------
 src/parsing/scope.ml           | 38 +++++++++++++++++-----------
 tests/{OK => KO}/1103.lp       |  0
 tests/{OK => KO}/1103b.lp      |  0
 tests/OK/1035.lp               |  6 ++---
 tests/OK/1101.lp               | 10 ++++----
 tests/OK/922.lp                | 15 +++++-------
 tests/OK/Nat.lp                | 36 ++++++++++++++++++++++++---
 tests/OK/builtin_zero_succ.lp  | 11 ---------
 tests/OK/group.lp              | 12 ++++-----
 tests/OK/inductive.lp          | 39 ++++++++++++++---------------
 tests/OK/max-suc-alg.lp        | 22 ++++++++---------
 tests/OK/nat_id1.lp            |  6 ++---
 tests/OK/nat_id2.lp            | 13 ++++------
 tests/OK/natural.lp            | 45 ++++++++++++++++++++++++++++------
 tests/OK/plus_ac.lp            |  2 +-
 tests/OK/rewrite0.lp           | 19 ++++++--------
 tests/OK/rewrite1.lp           |  5 +---
 tests/OK/rewrite2.lp           | 13 +++-------
 tests/OK/tutorial.lp           | 13 +++-------
 tests/OK/xor.lp                | 12 ++++-----
 tests/export_raw_dk.sh         |  2 +-
 tests/regressions/hrs.expected | 12 ++++-----
 tests/regressions/xtc.expected | 14 +++++------
 29 files changed, 228 insertions(+), 203 deletions(-)
 rename tests/{OK => KO}/1103.lp (100%)
 rename tests/{OK => KO}/1103b.lp (100%)
 delete mode 100644 tests/OK/builtin_zero_succ.lp

diff --git a/CHANGES.md b/CHANGES.md
index bce9602d3..91ee68c98 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -8,6 +8,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/).
 ### Added
 
 - Add tactic `set`.
+- Decimal notation for integers.
 
 ### Fixed
 
@@ -15,8 +16,9 @@ and this project adheres to [Semantic Versioning](https://semver.org/).
 
 ### Changed
 
-- Option '--erasing' renamed into '--mapping'.
 - The export option `--requiring` does not require as argument a file with extension `.v` anymore: the argument must be a module name.
+- Option '--erasing' renamed into '--mapping'.
+- Builtins necessary for the decimal notation.
 
 ## 2.5.1 (2024-07-22)
 
diff --git a/doc/commands.rst b/doc/commands.rst
index 1d1e33c0f..3ee401f3c 100644
--- a/doc/commands.rst
+++ b/doc/commands.rst
@@ -275,14 +275,19 @@ identifiers for zero and the successor function (see hereafter); to
 use tactics on equality, one needs to define some specific builtins;
 etc.
 
-**notation for natural numbers** It is possible to use the standard
-decimal notation for natural numbers by defining the builtins ``"0"``
-and ``"+1"`` as follows:
+**decimal notation for integers** It is possible to use the standard
+decimal notation for integers by defining the builtins ``"0"`` to
+``"10"``, ``"+"``, ``"*"``, and ``"-"`` (optional):
 
 ::
 
-   builtin "0"  ≔ zero; // : N
-   builtin "+1" ≔ succ; // : N → N
+   builtin "0"  ≔ ...;  // : N
+   builtin "1"  ≔ ...;  // : N
+   ...
+   builtin "10" := ...; // : N
+   builtin "+" := ....; // : N → N → N
+   builtin "*" := ....; // : N → N → N
+   builtin "-" := ....; // : N → N // (optional)
    type 42;
 
 .. _opaque:
diff --git a/doc/terms.rst b/doc/terms.rst
index 08991bf2d..71b1efce9 100644
--- a/doc/terms.rst
+++ b/doc/terms.rst
@@ -8,7 +8,8 @@ Identifiers
 An identifier can be:
 
 * a *regular* identifier: ``/`` or an arbitrary non-empty sequence of
-  UTF-8 codepoints not among ``\t\r\n :,;`(){}[]".@$|?/``
+  UTF-8 codepoints not among ``\t\r\n :,;`(){}[]".@$|?/`` that is not
+  an integer number
 
 * an *escaped* identifier: an arbitrary sequence of characters
   enclosed between ``{|`` and ``|}``
@@ -76,8 +77,7 @@ A user-defined term can be either:
   variable in a rule left-hand side, applied to all the variables of
   the context.
 
-* an integer between 0 and 2^30-1 if the :ref:`builtins <builtin>`
-  ``"0"`` and ``"+1"`` are defined
+* an integer if the appropriate :ref:`builtins <builtin>` are defined
 
 * a term enclosed between square brackets ``[`` … ``]`` for explicitly
   giving the value of an argument declared as implicit
diff --git a/src/handle/query.ml b/src/handle/query.ml
index bebce0d7b..cdbdce63f 100644
--- a/src/handle/query.ml
+++ b/src/handle/query.ml
@@ -68,7 +68,8 @@ let handle : Sig_state.t -> proof_state option -> p_query -> result =
       None
   | P_query_verbose(i) ->
       let i = try int_of_string i with Failure _ ->
-        fatal pos "Too big number (max is %d)" max_int in
+                fatal pos "Too big number (max is %d)" max_int in
+      if i < 0 then fatal pos "Negative number";
       if Timed.(!Console.verbose) = 0 then
         (Timed.(Console.verbose := i);
          Console.out 1 "verbose %i" i)
@@ -84,8 +85,10 @@ let handle : Sig_state.t -> proof_state option -> p_query -> result =
   | P_query_prover(s) -> Timed.(Why3_tactic.default_prover := s); None
   | P_query_prover_timeout(n) ->
       let n = try int_of_string n with Failure _ ->
-        fatal pos "Too big number (max is %d)" max_int in
-      Timed.(Why3_tactic.timeout := n); None
+                fatal pos "Too big number (max is %d)" max_int in
+      if n < 0 then fatal pos "Negative number";
+      Timed.(Why3_tactic.timeout := n);
+      None
   | P_query_print(None) ->
       begin
         match ps with
diff --git a/src/parsing/lpLexer.ml b/src/parsing/lpLexer.ml
index ef1e3432d..8f3383963 100644
--- a/src/parsing/lpLexer.ml
+++ b/src/parsing/lpLexer.ml
@@ -92,8 +92,7 @@ type token =
   (* other tokens *)
   | DEBUG_FLAGS of (bool * string)
       (* Tuple constructor (with parens) required by Menhir. *)
-  | NAT of string
-  | NEG_NAT of string
+  | INT of string
   | FLOAT of string
   | SIDE of Pratter.associativity
   | STRINGLIT of string
@@ -132,10 +131,9 @@ type token =
 (** Some regexp definitions. *)
 let space = [%sedlex.regexp? Chars " \t\n\r"]
 let digit = [%sedlex.regexp? '0' .. '9']
-let pos = [%sedlex.regexp? ('1' .. '9', Star digit)]
-let nat = [%sedlex.regexp? '0' | pos]
-let neg_nat = [%sedlex.regexp? '-', pos]
-let float = [%sedlex.regexp? (nat | neg_nat), '.', Plus digit]
+let nat = [%sedlex.regexp? Star digit]
+let int = [%sedlex.regexp? nat | '-', nat]
+let float = [%sedlex.regexp? int, '.', Plus digit]
 let oneline_comment = [%sedlex.regexp? "//", Star (Compl ('\n' | '\r'))]
 let string = [%sedlex.regexp? '"', Star (Compl '"'), '"']
 
@@ -266,8 +264,7 @@ let rec token lb =
   (* other tokens *)
   | '+', Plus lowercase -> DEBUG_FLAGS(true, remove_first lb)
   | '-', Plus lowercase -> DEBUG_FLAGS(false, remove_first lb)
-  | neg_nat -> NEG_NAT(Utf8.lexeme lb)
-  | nat -> NAT(Utf8.lexeme lb)
+  | int -> INT(Utf8.lexeme lb)
   | float -> FLOAT(Utf8.lexeme lb)
   | string -> STRINGLIT(Utf8.sub_lexeme lb 1 (lexeme_length lb - 2))
 
diff --git a/src/parsing/lpParser.mly b/src/parsing/lpParser.mly
index c95a03c2d..53322fa09 100644
--- a/src/parsing/lpParser.mly
+++ b/src/parsing/lpParser.mly
@@ -85,8 +85,7 @@
 // other tokens
 
 %token <bool * string> DEBUG_FLAGS
-%token <string> NAT
-%token <string> NEG_NAT
+%token <string> INT
 %token <string> FLOAT
 %token <Pratter.associativity> SIDE
 %token <string> STRINGLIT
@@ -150,7 +149,7 @@ search_query_alone:
     { q }
 
 command:
-  | OPAQUE i=qid_or_int SEMICOLON { make_pos $sloc (P_opaque i) }
+  | OPAQUE i=qid SEMICOLON { make_pos $sloc (P_opaque i) }
   | REQUIRE OPEN l=list(path) SEMICOLON
     { make_pos $sloc (P_require(true,l)) }
   | REQUIRE l=list(path) SEMICOLON
@@ -159,13 +158,13 @@ command:
     { make_pos $sloc (P_require_as(p,i)) }
   | OPEN l=list(path) SEMICOLON
     { make_pos $sloc (P_open l) }
-  | ms=modifier* SYMBOL s=uid_or_int al=param_list* COLON a=term
+  | ms=modifier* SYMBOL s=uid al=param_list* COLON a=term
     po=proof? SEMICOLON
     { let sym =
         {p_sym_mod=ms; p_sym_nam=s; p_sym_arg=al; p_sym_typ=Some(a);
          p_sym_trm=None; p_sym_def=false; p_sym_prf=po}
       in make_pos $sloc (P_symbol(sym)) }
-  | ms=modifier* SYMBOL s=uid_or_int al=param_list* ao=preceded(COLON, term)?
+  | ms=modifier* SYMBOL s=uid al=param_list* ao=preceded(COLON, term)?
     ASSIGN tp=term_proof SEMICOLON
     { let sym =
         {p_sym_mod=ms; p_sym_nam=s; p_sym_arg=al; p_sym_typ=ao;
@@ -176,11 +175,11 @@ command:
       { make_pos $sloc (P_inductive(Option.to_list exp,xs,is)) }
   | RULE rs=separated_nonempty_list(WITH, rule) SEMICOLON
       { make_pos $sloc (P_rules(rs)) }
-  | BUILTIN s=STRINGLIT ASSIGN i=qid_or_int SEMICOLON
+  | BUILTIN s=STRINGLIT ASSIGN i=qid SEMICOLON
     { make_pos $loc (P_builtin(s,i)) }
   | COERCE_RULE r=rule SEMICOLON { make_pos $loc (P_coercion r) }
   | UNIF_RULE r=unif_rule SEMICOLON { make_pos $loc (P_unif_rule(r)) }
-  | NOTATION i=qid_or_int n=notation SEMICOLON
+  | NOTATION i=qid n=notation SEMICOLON
     { make_pos $loc (P_notation(i,n)) }
   | q=query SEMICOLON { make_pos $sloc (P_query(q)) }
   | EOF { raise End_of_file }
@@ -202,9 +201,9 @@ query:
     { let (b, s) = fl in make_pos $sloc (P_query_debug(b, s)) }
   | FLAG s=STRINGLIT b=SWITCH { make_pos $sloc (P_query_flag(s,b)) }
   | PROVER s=STRINGLIT { make_pos $sloc (P_query_prover(s)) }
-  | PROVER_TIMEOUT n=NAT
+  | PROVER_TIMEOUT n=INT
     { make_pos $sloc (P_query_prover_timeout n) }
-  | VERBOSE n=NAT { make_pos $sloc (P_query_verbose n) }
+  | VERBOSE n=INT { make_pos $sloc (P_query_verbose n) }
   | TYPE_QUERY t=term
     { make_pos $sloc (P_query_infer(t, {strategy=NONE; steps=None}))}
   | SEARCH s=STRINGLIT
@@ -238,14 +237,6 @@ exposition:
 
 uid: s=UID { make_pos $sloc s}
 
-uid_or_int:
-  | i=uid { i }
-  | n=int { make_pos $sloc n }
-
-qid_or_int:
-  | i=qid { i }
-  | n=int { make_pos $sloc ([],n) }
-
 param_list:
   | x=param { ([x], None, false) }
   | L_PAREN xs=param+ COLON a=term R_PAREN { (xs, Some(a), false) }
@@ -254,7 +245,6 @@ param_list:
 
 param:
   | s=uid { Some s }
-  | n=NAT { Some (make_pos $sloc n) }
   | UNDERSCORE { None }
 
 term:
@@ -289,8 +279,7 @@ aterm:
       make_pos $sloc (P_Patt(i, Option.map Array.of_list e)) }
   | L_PAREN t=term R_PAREN { make_pos $sloc (P_Wrap(t)) }
   | L_SQ_BRACKET t=term R_SQ_BRACKET { make_pos $sloc (P_Expl(t)) }
-  | n=NAT { make_pos $sloc (P_NLit n) }
-  | n=NEG_NAT { make_pos $sloc (P_Iden(make_pos $sloc ([],n), false)) }
+  | n=INT { make_pos $sloc (P_NLit n) }
 
 env: DOT L_SQ_BRACKET ts=separated_list(SEMICOLON, term) R_SQ_BRACKET { ts }
 
@@ -349,7 +338,7 @@ tactic:
   | REWRITE d=SIDE? p=rw_patt_spec? t=term
     { let b = match d with Some Pratter.Left -> false | _ -> true in
       make_pos $sloc (P_tac_rewrite(b,p,t)) }
-  | SIMPLIFY i=qid_or_int? { make_pos $sloc (P_tac_simpl i) }
+  | SIMPLIFY i=qid? { make_pos $sloc (P_tac_simpl i) }
   | SOLVE { make_pos $sloc P_tac_solve }
   | SYMMETRY { make_pos $sloc P_tac_sym }
   | TRY t=tactic { make_pos $sloc (P_tac_try t) }
@@ -378,7 +367,7 @@ inductive: i=uid ps=param_list* COLON t=term ASSIGN
     { let t = make_prod $startpos(ps) ps t $endpos(t) in
       make_pos $sloc (i,t,l) }
 
-constructor: i=uid_or_int ps=param_list* COLON t=term
+constructor: i=uid ps=param_list* COLON t=term
     { (i, make_prod $startpos(ps) ps t $endpos(t)) }
 
 rule: l=term HOOK_ARROW r=term { make_pos $sloc (l, r) }
@@ -407,11 +396,7 @@ notation:
 
 float_or_int:
   | s=FLOAT { s }
-  | s=int { s }
-
-int:
-  | s=NEG_NAT { s }
-  | s=NAT { s }
+  | s=INT { s }
 
 maybe_generalize:
   | g = GENERALIZE?
diff --git a/src/parsing/scope.ml b/src/parsing/scope.ml
index f0381dc9d..6b76ba7df 100644
--- a/src/parsing/scope.ml
+++ b/src/parsing/scope.ml
@@ -165,6 +165,9 @@ let _ =
   assert (valid "case_ex02_intro1");
   assert (valid "case_ex02_intro10")
 
+(* used in desugaring decimal notations *)
+let strint = Array.init 11 string_of_int
+
 (** [scope ~find_sym ~typ k md ss env t] turns a parser-level term [t] into an
     actual term. *)
 let rec scope : ?find_sym:find_sym ->
@@ -323,21 +326,28 @@ and scope_head : ?find_sym:find_sym ->
   | (P_Iden(qid,_), _) -> scope_iden ?find_sym md ss env qid
 
   | (P_NLit(s), _) ->
-    begin
-      let n = try int_of_string s with Failure _ ->
-        fatal t.pos "Too big number (max is %d)." max_int
+      let neg, s =
+        let neg = s.[0] = '-' in
+        let s = if neg then String.sub s 1 (String.length s - 1) else s in
+        neg, s
+      in
+      let sym_of s = _Symb (Builtin.get ss t.pos s) in
+      let sym = Array.map sym_of strint in
+      let digit = function
+        | '0' -> sym.(0) | '1' -> sym.(1) | '2' -> sym.(2) | '3' -> sym.(3)
+        | '4' -> sym.(4) | '5' -> sym.(5) | '6' -> sym.(6) | '7' -> sym.(7)
+        | '8' -> sym.(8) | '9' -> sym.(9) | _ -> assert false
+      in
+      let sym_add = sym_of "+" in
+      let add x y = _Appl (_Appl sym_add x) y in
+      let sym_mul = sym_of "*" in
+      let mul x y = _Appl (_Appl sym_mul x) y in
+      let rec unsugar i =
+        if i <= 0 then digit s.[0]
+        else add (digit s.[i]) (mul sym.(10) (unsugar (i-1)))
       in
-      match Builtin.get_opt ss "0" with
-      | None -> scope_iden md ss env {t with elt=([],s)}
-      | Some sym_z ->
-        match Builtin.get_opt ss "+1" with
-        | None -> scope_iden md ss env {t with elt=([],s)}
-        | Some sym_s ->
-          let z = _Symb sym_z and s = _Symb sym_s in
-          let rec unsugar_nat_lit acc n =
-            if n <= 0 then acc else unsugar_nat_lit (_Appl s acc) (n-1) in
-          unsugar_nat_lit z n
-    end
+      let n = unsugar (String.length s - 1) in
+      if neg then _Appl (sym_of "-") n else n
 
   | (P_Wild, M_URHS(data)) ->
     let x =
diff --git a/tests/OK/1103.lp b/tests/KO/1103.lp
similarity index 100%
rename from tests/OK/1103.lp
rename to tests/KO/1103.lp
diff --git a/tests/OK/1103b.lp b/tests/KO/1103b.lp
similarity index 100%
rename from tests/OK/1103b.lp
rename to tests/KO/1103b.lp
diff --git a/tests/OK/1035.lp b/tests/OK/1035.lp
index ba1a60078..cbbe6c252 100644
--- a/tests/OK/1035.lp
+++ b/tests/OK/1035.lp
@@ -1,18 +1,18 @@
 symbol Set:TYPE;
 injective symbol τ:Set → TYPE;
 symbol ℕ:TYPE;
-symbol 0:ℕ;
+symbol O:ℕ;
 symbol 𝑰 [a]: ℕ → τ a;
 
 symbol code_S' : Set;
 symbol S' ≔ τ code_S';
 //print S';
 //debug +uv;
-symbol a':S' ≔ 𝑰 0;
+symbol a':S' ≔ 𝑰 O;
 //debug -uv;
 
 private symbol code_S : Set;
 private symbol S ≔ τ code_S;
 //print S;
 //debug +uv;
-private symbol a: S ≔ 𝑰 0;
+private symbol a: S ≔ 𝑰 O;
diff --git a/tests/OK/1101.lp b/tests/OK/1101.lp
index c428b9a0a..217abd259 100644
--- a/tests/OK/1101.lp
+++ b/tests/OK/1101.lp
@@ -38,26 +38,26 @@ builtin "refl"  ≔ eq_refl;
 builtin "eqind" ≔ ind_eq;
 
 symbol nat:Set;
-symbol 0:τ nat;
+symbol O:τ nat;
 symbol +:τ(nat ↦ nat ↦ nat);
 notation + infix right 20;
-rule $x + 0 ↪ $x;
+rule $x + O ↪ $x;
 symbol f:τ(nat ↦ (nat ↦ nat) ↦ nat);
 symbol add_com a b : π(a + b = b + a);
 
-symbol test1 a b : π (f (a + b) (λ _, 0) = f (b + a) (λ _, 0))
+symbol test1 a b : π (f (a + b) (λ _, O) = f (b + a) (λ _, O))
 ≔ begin
   assume a b;
   rewrite add_com;
   reflexivity
 end;
 
-symbol test2' a b : π (f (a + b) (λ _, 0) = f (b + a) (λ _, 0))
+symbol test2' a b : π (f (a + b) (λ _, O) = f (b + a) (λ _, O))
 ≔ begin
   assume a b;
   simplify;
   set p ≔ (a + b);
-  set g ≔ (a + b + 0 + 0);
+  set g ≔ (a + b + O + O);
   //type p;
   //compute p;
   //compute g;
diff --git a/tests/OK/922.lp b/tests/OK/922.lp
index 8ef5ccfee..26f7c4508 100644
--- a/tests/OK/922.lp
+++ b/tests/OK/922.lp
@@ -1,7 +1,7 @@
 require open tests.OK.Set tests.OK.Prop tests.OK.Eq tests.OK.Bool;
 
 inductive ℕ : TYPE ≔
-| 0 : ℕ
+| O : ℕ
 | +1 : ℕ → ℕ;
 
 constant symbol nat : Set;
@@ -10,15 +10,12 @@ rule τ nat ↪ ℕ;
 
 notation +1 postfix 10;
 
-builtin "0"  ≔ 0;
-builtin "+1" ≔ +1;
+symbol isO : ℕ → 𝔹;
 
-symbol is0 : ℕ → 𝔹;
+rule isO O ↪ true
+with isO (_ +1) ↪ false;
 
-rule is0 0 ↪ true
-with is0 (_ +1) ↪ false;
-
-opaque symbol s≠0 [n] : π (n +1 ≠ 0) ≔
+opaque symbol s≠O [n] : π (n +1 ≠ O) ≔
 begin
-  assume n h; refine ind_eq h (λ n, istrue(is0 n)) ⊤ᵢ
+  assume n h; refine ind_eq h (λ n, istrue(isO n)) ⊤ᵢ
 end;
diff --git a/tests/OK/Nat.lp b/tests/OK/Nat.lp
index fb9f531cf..8313aa230 100644
--- a/tests/OK/Nat.lp
+++ b/tests/OK/Nat.lp
@@ -1,14 +1,42 @@
 require open tests.OK.Set tests.OK.Prop tests.OK.Eq tests.OK.Bool;
 
 inductive ℕ : TYPE ≔
-| 0 : ℕ
+| O : ℕ
 | +1 : ℕ → ℕ; notation +1 postfix 100;
 
-builtin "0"  ≔ 0;
-builtin "+1" ≔ +1;
-
 constant symbol nat : Set;
 
 rule τ nat ↪ ℕ;
 
 symbol + : ℕ → ℕ → ℕ; notation + infix 20;
+symbol × : ℕ → ℕ → ℕ; notation + infix 20;
+
+// Enabling decimal notation
+
+symbol n1 ≔ O +1;
+symbol n2 ≔ n1 +1;
+symbol n3 ≔ n2 +1;
+symbol n4 ≔ n3 +1;
+symbol n5 ≔ n4 +1;
+symbol n6 ≔ n5 +1;
+symbol n7 ≔ n6 +1;
+symbol n8 ≔ n7 +1;
+symbol n9 ≔ n8 +1;
+symbol n10 ≔ n9 +1;
+
+builtin "0"  ≔ O;
+builtin "1" ≔ n1;
+builtin "2" ≔ n2;
+builtin "3" ≔ n3;
+builtin "4" ≔ n4;
+builtin "5" ≔ n5;
+builtin "6" ≔ n6;
+builtin "7" ≔ n7;
+builtin "8" ≔ n8;
+builtin "9" ≔ n9;
+builtin "10" ≔ n10;
+
+builtin "+" ≔ +;
+builtin "*" ≔ ×;
+
+symbol forty_two ≔ 42;
diff --git a/tests/OK/builtin_zero_succ.lp b/tests/OK/builtin_zero_succ.lp
deleted file mode 100644
index 8cd2fdeae..000000000
--- a/tests/OK/builtin_zero_succ.lp
+++ /dev/null
@@ -1,11 +0,0 @@
-symbol N:TYPE;
-symbol z:N;
-symbol s:N → N;
-builtin "0" ≔ z;
-builtin "+1" ≔ s;
-symbol +:N → N → N;
-notation + infix 5;
-rule 0 + $y ↪ $y
-with s $x + $y ↪ s($x + $y);
-compute 5 + 5;
-assert ⊢ 5 + 5 ≡ 10;
diff --git a/tests/OK/group.lp b/tests/OK/group.lp
index 30c5c475d..c962aa1d8 100644
--- a/tests/OK/group.lp
+++ b/tests/OK/group.lp
@@ -1,16 +1,16 @@
 // decision procedure for group theory
 symbol G : TYPE;
-symbol 1 : G;
+symbol e : G;
 symbol ⋅ : G → G → G;
 notation ⋅ infix 10;
 symbol inv : G → G;
 rule ($x ⋅ $y) ⋅ $z ↪ $x ⋅ ($y ⋅ $z)
-with 1 ⋅ $x ↪ $x
-with $x ⋅ 1 ↪ $x
-with inv $x ⋅ $x ↪ 1
-with $x ⋅ inv $x ↪ 1
+with e ⋅ $x ↪ $x
+with $x ⋅ e ↪ $x
+with inv $x ⋅ $x ↪ e
+with $x ⋅ inv $x ↪ e
 with inv $x ⋅ ($x ⋅ $y) ↪ $y
 with $x ⋅ (inv $x ⋅ $y) ↪ $y
-with inv 1 ↪ 1
+with inv e ↪ e
 with inv (inv $x) ↪ $x
 with inv ($x ⋅ $y) ↪ inv $y ⋅ inv $x;
diff --git a/tests/OK/inductive.lp b/tests/OK/inductive.lp
index 64e2d222d..574b2e3fe 100644
--- a/tests/OK/inductive.lp
+++ b/tests/OK/inductive.lp
@@ -109,17 +109,14 @@ assert p pz psucc n ⊢ ind_N p pz psucc (succ n) ≡ psucc n (ind_N p pz psucc
 constant symbol nat : Set;
 rule τ nat ↪ N;
 
-builtin "0"  ≔ z;
-builtin "+1" ≔ succ;
-
 symbol + : N → N → N;
 notation + infix left 6;
-rule       0 + $y ↪ $y
+rule       z + $y ↪ $y
 with succ $x + $y ↪ succ ($x + $y);
 
 symbol × : N → N → N;
 notation × infix left 7;
-rule       0 × _  ↪ 0
+rule       z × _  ↪ z
 with succ $x × $y ↪ $y + $x × $y;
 
 assert x y z ⊢ x + y × z ≡ x + (y × z);
@@ -336,27 +333,27 @@ c2 (ind_CExp pA pB pC paLit paAdd paIf pbLit pbEq pcSkip pcAss pcSeq pcIf c2);
 ////////////////////// Even and odd
 
 inductive even : N → TYPE ≔
-  | even_O : even 0
+  | even_O : even z
   | even_S : Π n, odd n → even (succ n)
 with odd : N → TYPE ≔
   | odd_S : Π n, even n → odd (succ n);
 
 assert ⊢ even : N → TYPE;
-assert ⊢ even_O : even 0;
+assert ⊢ even_O : even z;
 assert ⊢ even_S : Π n, odd n → even (succ n);
 assert ⊢ odd : N → TYPE;
 assert ⊢ odd_S : Π n, even n → odd (succ n);
 
 assert ⊢ ind_even :
   Π p0: Π x: N, even x → Prop, Π p1: Π x: N, odd x → Prop,
-    π(p0 0 even_O) →
+    π(p0 z even_O) →
    (Π n: τ nat, Π x: odd n, π(p1 n x) → π(p0 (succ n) (even_S n x))) →
    (Π n: τ nat, Π x: even n, π(p0 n x) → π(p1 (succ n) (odd_S n x))) →
   Π x: N, Π x0: even x, π(p0 x x0);
 
 assert ⊢ ind_odd :
   Π p0: Π x: N, even x → Prop, Π p1: Π x: N, odd x → Prop,
-    π(p0 0 even_O) →
+    π(p0 z even_O) →
     (Π n: τ nat, Π x: odd n, π(p1 n x) → π(p0 (succ n) (even_S n x))) →
     (Π n: τ nat, Π x: even n, π(p0 n x) → π(p1 (succ n) (odd_S n x))) →
   Π x: N, Π x0: odd x, π(p1 x x0);
@@ -565,19 +562,19 @@ assert p pnil pcons b x xb l
 
 inductive rom : N → TYPE ≔
  | mty : rom z // leaf node
- | bin : Π e1 e2, rom e1 → rom e2 → rom (e1 + e2 + 1)  // binary nodes
- | unl : Π e k, π(k ≤ 2 × e) → rom e → rom (succ e); // unary labeled nodes
+ | bin : Π e1 e2, rom e1 → rom e2 → rom (e1 + e2 + succ z)  // binary nodes
+ | unl : Π e k, π(k ≤ (succ(succ z)) × e) → rom e → rom (succ e); // unary labeled nodes
 
 assert ⊢ rom : N → TYPE;
 assert ⊢ mty : rom z;
-assert ⊢ bin : Π e1 e2, rom e1 → rom e2 → rom (e1 + e2 + 1);
-assert ⊢ unl : Π e k, π(k ≤ 2 × e) → rom e → rom (succ e);
+assert ⊢ bin : Π e1 e2, rom e1 → rom e2 → rom (e1 + e2 + succ z);
+assert ⊢ unl : Π e k, π(k ≤ (succ(succ z)) × e) → rom e → rom (succ e);
 
 assert ⊢ ind_rom : Π p: Π x: N, rom x → Prop,
-  π(p 0 mty) →
+  π(p z mty) →
   (Π e1:N, Π e2:N, Π x:rom e1, π(p e1 x) → Π x0:rom e2, π(p e2 x0) →
-     π(p ((e1 + e2) + 1) (bin e1 e2 x x0))) → 
-  (Π e:N, Π k:N, Π x:π(k ≤ (2 × e)), Π x0:rom e, π(p e x0) →
+     π(p ((e1 + e2) + succ z) (bin e1 e2 x x0))) → 
+  (Π e:N, Π k:N, Π x:π(k ≤ ((succ(succ z)) × e)), Π x0:rom e, π(p e x0) →
     π(p (succ e) (unl e k x x0))) → 
   Π x:N, Π x0:rom x, π(p x x0);
 
@@ -611,8 +608,8 @@ assert ⊢ ind_fibo : Π p: Π x: N, Π x0: N, fibo x x0 → Prop,
      Π x0: fibo n r1, π(p n r1 x0) →
      Π x1: fibo (succ n) r2, π(p (succ n) r2 x1) →
   π(p (succ (succ n)) (r1 + r2) (cgen' n r1 r2 x0 x1))) →
-  π(p 0 1 cbase1) →
-  π(p 1 1 cbase2) →
+  π(p z (succ z) cbase1) →
+  π(p (succ z) (succ z) cbase2) →
   Π x:N, Π x0:N, Π x1:fibo x x0, π(p x x0 x1);
 
 assert p pcgen' pcbase1 pcbase2 n r1 r2 hypF1 hypF2
@@ -664,13 +661,13 @@ builtin "eqind" ≔ eq_ind;
 // Some proofs
 /////////////////////////////
 
-opaque symbol plus_0_n n : π(0 + n = n) ≔
+opaque symbol plus_0_n n : π(z + n = n) ≔
 begin
   assume n;
   reflexivity
 end;
 
-opaque symbol plus_n_0 (n:N) : π(n + 0 = n) ≔
+opaque symbol plus_n_0 (n:N) : π(n + z = n) ≔
 begin
   induction
   {// Case n = O
@@ -685,7 +682,7 @@ end;
 // About lists
 
 symbol length : List → N;
-rule length nil ↪ 0
+rule length nil ↪ z
  with length (cons _ $l) ↪ succ (length $l);
 
 symbol app : List → List → List;
diff --git a/tests/OK/max-suc-alg.lp b/tests/OK/max-suc-alg.lp
index 2669171c7..e7ce5d983 100644
--- a/tests/OK/max-suc-alg.lp
+++ b/tests/OK/max-suc-alg.lp
@@ -7,21 +7,21 @@ symbol V : L → L; // to mark universe level variables
 
 // natural numbers
 constant symbol ℕ : TYPE;
-constant symbol 0ₙ : ℕ; builtin "0" ≔ 0ₙ;
-constant symbol sₙ : ℕ → ℕ; builtin "+1" ≔ sₙ;
+constant symbol Oₙ : ℕ;
+constant symbol sₙ : ℕ → ℕ;
 
 // max function on natural numbers
 symbol ⊕ₙ : ℕ → ℕ → ℕ; notation ⊕ₙ infix right 10;
 
-rule 0ₙ ⊕ₙ $y ↪ $y
-with $x ⊕ₙ 0ₙ ↪ $x
+rule Oₙ ⊕ₙ $y ↪ $y
+with $x ⊕ₙ Oₙ ↪ $x
 with sₙ $x ⊕ₙ sₙ $y ↪ sₙ ($x ⊕ₙ $y);
 
 // addition on natural numbers
 symbol + : ℕ → ℕ → ℕ; notation + infix right 5;
 
-rule 0ₙ + $y ↪ $y
-with $x + 0ₙ ↪ $x
+rule Oₙ + $y ↪ $y
+with $x + Oₙ ↪ $x
 with sₙ $x + $y ↪ sₙ ($x + $y)
 with $x + sₙ $y ↪ sₙ ($x + $y)
 with ($x + $y) + $z ↪ $x + ($y + $z);
@@ -33,10 +33,10 @@ associative commutative symbol ⊕ : L → L → L; // associative right by defa
 notation ⊕ infix right 10;
 
 // Translation of Agda's levels to the s-max algebra 
-rule Z       ↪ s 0 z
-with S $x    ↪ s 1 $x
+rule Z       ↪ s Oₙ z
+with S $x    ↪ s (sₙ Oₙ) $x
 with $x ∪ $y ↪ $x ⊕ $y
-with V $x    ↪ s 0 ($x ⊕ z);
+with V $x    ↪ s Oₙ ($x ⊕ z);
 
 // rules for deciding the s-max algebra
 rule s $p (s $q $x) ↪ s ($p + $q) $x
@@ -46,5 +46,5 @@ rule s $p $x ⊕ s $q $x ↪ s ($p ⊕ₙ $q) $x
 with s $p $x ⊕ (s $q $x ⊕ $y) ↪ s ($p ⊕ₙ $q) $x ⊕ $y;
 
 // tests
-assert x y ⊢ ((S (S (V x))) ∪ (S (V y))) ∪ Z ≡ s 1 y ⊕ (s 2 x ⊕ s 2 z);
-assert a ⊢ s 1 (a ⊕ z) ⊕ s 2 (a ⊕ z) ≡ s 2 a ⊕ s 2 z;
+assert x y ⊢ ((S (S (V x))) ∪ (S (V y))) ∪ Z ≡ s (sₙ Oₙ) y ⊕ (s (sₙ(sₙ Oₙ)) x ⊕ s (sₙ(sₙ Oₙ)) z);
+assert a ⊢ s (sₙ Oₙ) (a ⊕ z) ⊕ s (sₙ(sₙ Oₙ)) (a ⊕ z) ≡ s (sₙ(sₙ Oₙ)) a ⊕ s (sₙ(sₙ Oₙ)) z;
diff --git a/tests/OK/nat_id1.lp b/tests/OK/nat_id1.lp
index 9a56280a9..06d56b226 100644
--- a/tests/OK/nat_id1.lp
+++ b/tests/OK/nat_id1.lp
@@ -1,9 +1,9 @@
 symbol G:TYPE;
 
-symbol 1:G;
+symbol e:G;
 
-compute 1;
+compute e;
 
 symbol *:G → G → G; notation * infix 10;
 
-compute 1 * 1;
+compute e * e;
diff --git a/tests/OK/nat_id2.lp b/tests/OK/nat_id2.lp
index 71f017ca3..d8288d2fa 100644
--- a/tests/OK/nat_id2.lp
+++ b/tests/OK/nat_id2.lp
@@ -1,10 +1,7 @@
 symbol N:TYPE;
 
-symbol 0:N; builtin "0" ≔ 0;
-symbol s:N → N; builtin "+1" ≔ s;
-
-compute 0;
-compute 3;
+symbol O:N;
+symbol s:N → N;
 
 symbol G:TYPE;
 
@@ -16,8 +13,8 @@ with e * $x ↪ $x;
 
 symbol ⋅:N → G → G; notation ⋅ infix 20;
 
-rule 0 ⋅ $x ↪ e
+rule O ⋅ $x ↪ e
 with s $n ⋅ $x ↪ $x * $n ⋅ $x;
 
-compute λ x, 0 ⋅ x;
-compute λ x, 3 ⋅ x;
+compute λ x, O ⋅ x;
+compute λ x, (s(s(s O))) ⋅ x;
diff --git a/tests/OK/natural.lp b/tests/OK/natural.lp
index e8822b8f5..06a021ffb 100644
--- a/tests/OK/natural.lp
+++ b/tests/OK/natural.lp
@@ -7,13 +7,6 @@ constant symbol N : TYPE;
 constant symbol z : N;
 constant symbol s : N → N;
 
-// Enabling built-in natural number literal, and example.
-
-builtin "0"  ≔ z;
-builtin "+1" ≔ s;
-
-symbol forty_two ≔ 42;
-
 // Addition function.
 
 symbol + : N → N → N;
@@ -34,6 +27,44 @@ with (s $m) × $n     ↪ $n + $m × $n
 with _      × z      ↪ z
 with $m     × (s $n) ↪ $m + $m × $n;
 
+// Enabling decimal notation
+
+symbol n1 ≔ s z;
+symbol n2 ≔ s n1;
+symbol n3 ≔ s n2;
+symbol n4 ≔ s n3;
+symbol n5 ≔ s n4;
+symbol n6 ≔ s n5;
+symbol n7 ≔ s n6;
+symbol n8 ≔ s n7;
+symbol n9 ≔ s n8;
+symbol n10 ≔ s n9;
+
+builtin "0"  ≔ z;
+builtin "1" ≔ n1;
+builtin "2" ≔ n2;
+builtin "3" ≔ n3;
+builtin "4" ≔ n4;
+builtin "5" ≔ n5;
+builtin "6" ≔ n6;
+builtin "7" ≔ n7;
+builtin "8" ≔ n8;
+builtin "9" ≔ n9;
+builtin "10" ≔ n10;
+
+builtin "+" ≔ +;
+builtin "*" ≔ ×;
+
+symbol forty_two ≔ 42;
+
+//print forty_two;
+
+assert ⊢ forty_two
+  ≡ let two ≔ s(s z) in
+    let four ≔ two + two in
+    let ten ≔ four + four + two in
+    four × ten + two;
+
 // Doubling function.
 
 symbol double n ≔ n × 2;
diff --git a/tests/OK/plus_ac.lp b/tests/OK/plus_ac.lp
index a4158a143..7f0ddc623 100644
--- a/tests/OK/plus_ac.lp
+++ b/tests/OK/plus_ac.lp
@@ -1,5 +1,5 @@
 symbol N:TYPE;
-symbol 0:N;
+symbol O:N;
 symbol s:N → N;
 associative commutative symbol +:N → N → N;
 notation + infix 10;
diff --git a/tests/OK/rewrite0.lp b/tests/OK/rewrite0.lp
index 3b113df3f..2d2fd43c4 100644
--- a/tests/OK/rewrite0.lp
+++ b/tests/OK/rewrite0.lp
@@ -26,16 +26,13 @@ symbol N ≔ T nat;
 constant symbol z : N;
 constant symbol s : N → N;
 
-builtin "0"  ≔ z;
-builtin "+1" ≔ s;
-
 // Addition on natural numbers.
 
 symbol + : N → N → N;
 
 notation + infix left 3;
 
-rule 0 + $x ↪ $x
+rule z + $x ↪ $x
 with s $x + $y ↪ s ($x + $y);
 
 // Multiplication on natural numbers.
@@ -44,7 +41,7 @@ symbol * : N → N → N;
 
 notation * infix left 4;
 
-rule 0 * _  ↪ 0
+rule z * _  ↪ z
 with s $x * $y ↪ $y + $x * $y;
 
 // Type of propositions and their interpretation as types.
@@ -59,19 +56,19 @@ rule P (all $f) ↪ Π x, P ($f x);
 
 // Induction principle on N.
 
-symbol nat_ind p : P(p 0) → (Π n, P(p n) → P(p (s n))) → Π n, P(p n);
+symbol nat_ind p : P(p z) → (Π n, P(p n) → P(p (s n))) → Π n, P(p n);
 
-rule nat_ind _  $u _  0      ↪ $u
+rule nat_ind _  $u _  z      ↪ $u
 with nat_ind $p $u $v (s $n) ↪ $v $n (nat_ind $p $u $v $n);
 
 // Boolean equality on N.
 
 symbol beq : N → N → B;
 
-rule beq 0      0      ↪ true
+rule beq z      z      ↪ true
 with beq (s $x) (s $y) ↪ beq $x $y
-with beq 0      (s _ ) ↪ false
-with beq (s _ ) 0      ↪ false;
+with beq z      (s _ ) ↪ false
+with beq (s _ ) z      ↪ false;
 
 // Leibniz equality.
 
@@ -97,7 +94,7 @@ opaque symbol add_succ_r n m : P (n + s m = s (n + m))
 ≔ begin
   assume n m;
   refine nat_ind (λ n, n + s m = s (n + m)) _ _ n
-  { // Case 0;
+  { // Case z;
   simplify;
   reflexivity }
   { // Case s;
diff --git a/tests/OK/rewrite1.lp b/tests/OK/rewrite1.lp
index 48d748029..61754f88b 100644
--- a/tests/OK/rewrite1.lp
+++ b/tests/OK/rewrite1.lp
@@ -12,9 +12,6 @@ constant symbol N : TYPE;
 constant symbol z : N;
 constant symbol s : N → N;
 
-builtin "0"  ≔ z;
-builtin "+1" ≔ s;
-
 // Addition on natural numbers.
 
 symbol add : N → N → N;
@@ -165,7 +162,7 @@ opaque symbol addcomm : Π n m, P (eq nat (add n m) (add m n))
 end;
 
 // Adding the same value is the same as multiplying by 2.
-opaque symbol add_same_times_two : Π x, P (eq nat (add x x) (mul 2 x))
+opaque symbol add_same_times_two : Π x, P (eq nat (add x x) (mul (s(s z)) x))
 ≔ begin
   assume x;
   simplify;
diff --git a/tests/OK/rewrite2.lp b/tests/OK/rewrite2.lp
index d68ebc562..87803f3d4 100644
--- a/tests/OK/rewrite2.lp
+++ b/tests/OK/rewrite2.lp
@@ -61,23 +61,18 @@ constant symbol nat : Set;
 
 rule τ nat ↪ ℕ;
 
-// Enabling the use of decimal notation
-
-builtin "0"  ≔ zero;
-builtin "+1" ≔ s;
-
 // Addition
 
 symbol + : ℕ → ℕ → ℕ;
 
 notation + infix left 20;
 
-rule 0 + $y ↪ $y
+rule zero + $y ↪ $y
 with s $x + $y ↪ s ($x + $y);
 
 // Addition is commutative
 
-opaque symbol add0r x : π (x + 0 = x) ≔
+opaque symbol add0r x : π (x + zero = x) ≔
 begin
   induction
   {// case x = 0
@@ -86,7 +81,7 @@ begin
   assume x' h; simplify; rewrite h; reflexivity}
 end;
 
-rule $x + 0 ↪ $x;
+rule $x + zero ↪ $x;
 
 opaque symbol addsr x y : π (x + s y = s (x + y)) ≔
 begin
@@ -135,7 +130,7 @@ end;
 
 symbol f : ℕ → (ℕ → ℕ) → ℕ;
 
-symbol test2 a b : π (f (a + b) (λ _, 0) = f (b + a) (λ _, 0))
+symbol test2 a b : π (f (a + b) (λ _, zero) = f (b + a) (λ _, zero))
 ≔ begin
   assume a b;
   rewrite add_com;
diff --git a/tests/OK/tutorial.lp b/tests/OK/tutorial.lp
index fbc2d9b0d..35e46cba7 100644
--- a/tests/OK/tutorial.lp
+++ b/tests/OK/tutorial.lp
@@ -25,19 +25,14 @@ symbol zero : ℕ; // is an object declaration
 symbol succ : ℕ → ℕ; /* means that "succ" takes an argument of type ℕ
   and returns something of type ℕ. */
 
-/* We can use the usual decimal notation for natural numbers by mapping
-Lambdapi builtin symbols to user-defined symbols: */
-builtin "0" ≔ zero;
-builtin "+1" ≔ succ;
-
 // We can make definitions as follows:
-symbol ten ≔ 10;
+symbol one ≔ succ zero;
 
 // We can ask Lambdapi the type of a term:
-type ten;
+type one;
 
 // We can check that a term has a given type:
-assert ⊢ ten : ℕ;
+assert ⊢ one : ℕ;
 
 // or that a term does not have a given type:
 assertnot ⊢ succ : ℕ;
@@ -268,7 +263,7 @@ rules:
   ind_Nat $v0_p0 $v1_z $v2_s z ↪ $v1_z
   ind_Nat $v0_p0 $v1_z $v2_s (s $v3_x0) ↪ $v2_s $v3_x0 (ind_Nat $v0_p0 $v1_z $v2_s $v3_x0)
 */
-print ten; // to see the definition of ten
+print one; // to see the definition of ten
 print +; // to see the type, notation and rules of +
 
 /* It is also possible now to replace the tactic "refine ind_Nat _ _ _"
diff --git a/tests/OK/xor.lp b/tests/OK/xor.lp
index af21f91cc..95f2e24cd 100644
--- a/tests/OK/xor.lp
+++ b/tests/OK/xor.lp
@@ -1,12 +1,12 @@
 symbol B:TYPE;
 
-symbol 0:B;
+symbol O:B;
 associative commutative symbol +:B → B → B; notation + infix right 20;
 
-rule 0 + $x ↪ $x
-with $x + 0 ↪ $x
-with $x + $x ↪ 0;
+rule O + $x ↪ $x
+with $x + O ↪ $x
+with $x + $x ↪ O;
 
-compute λ x, (x + 0) + (x + x + x);
+compute λ x, (x + O) + (x + x + x);
 
-assert x ⊢ x + 0 ≡ x + x + x;
+assert x ⊢ x + O ≡ x + x + x;
diff --git a/tests/export_raw_dk.sh b/tests/export_raw_dk.sh
index 05bcf28d7..b6badd6b9 100755
--- a/tests/export_raw_dk.sh
+++ b/tests/export_raw_dk.sh
@@ -52,7 +52,7 @@ do
         # "as"
         729);;
         # "notation"
-        xor|Set|quant*|Prop|prefix|parametricCoercions|opaque|nat_id*|michael|max-suc-alg|lpparse|861|infix|infer|indrec|implicitArgs[34]|group|cr_qu|cp*|coercions|builtin_zero_succ|plus_ac|693|693_assume|679|665|655|655b|649_fo_27|595_and_elim|584_c_slow|579_or_elim_long|579_long_no_duplicate|359|328|245|245b|244|1026|706|1101);;
+        xor|Set|quant*|Prop|prefix|parametricCoercions|opaque|nat_id*|michael|max-suc-alg|lpparse|861|infix|infer|indrec|implicitArgs[34]|group|cr_qu|cp*|coercions|plus_ac|693|693_assume|679|665|655|655b|649_fo_27|595_and_elim|584_c_slow|579_or_elim_long|579_long_no_duplicate|359|328|245|245b|244|1026|706|1101);;
         # "quantifier"
         683|650|573|565|430);;
         # nested module name
diff --git a/tests/regressions/hrs.expected b/tests/regressions/hrs.expected
index 14af77d9f..6aca15595 100644
--- a/tests/regressions/hrs.expected
+++ b/tests/regressions/hrs.expected
@@ -3,7 +3,7 @@ A : t -> t -> t
 L : t -> (t -> t) -> t
 P : t -> (t -> t) -> t
 B : t -> t -> (t -> t) -> t
-tests_OK_group_1 : t
+tests_OK_group_e : t
 tests_OK_group_inv : t
 tests_OK_group_⋅ : t
 )
@@ -29,14 +29,14 @@ $10_1 : t
 (RULES
 A(L($x,$y),$z) -> $y($z),
 B($x,$z,$y) -> $y($z),
-A(tests_OK_group_inv,tests_OK_group_1) -> tests_OK_group_1,
+A(tests_OK_group_inv,tests_OK_group_e) -> tests_OK_group_e,
 A(tests_OK_group_inv,A(tests_OK_group_inv,$2_0)) -> $2_0,
 A(tests_OK_group_inv,A(A(tests_OK_group_⋅,$3_0),$3_1)) -> A(A(tests_OK_group_⋅,A(tests_OK_group_inv,$3_1)),A(tests_OK_group_inv,$3_0)),
 A(A(tests_OK_group_⋅,A(A(tests_OK_group_⋅,$4_0),$4_1)),$4_2) -> A(A(tests_OK_group_⋅,$4_0),A(A(tests_OK_group_⋅,$4_1),$4_2)),
-A(A(tests_OK_group_⋅,tests_OK_group_1),$5_0) -> $5_0,
-A(A(tests_OK_group_⋅,$6_0),tests_OK_group_1) -> $6_0,
-A(A(tests_OK_group_⋅,A(tests_OK_group_inv,$7_0)),$7_0) -> tests_OK_group_1,
-A(A(tests_OK_group_⋅,$8_0),A(tests_OK_group_inv,$8_0)) -> tests_OK_group_1,
+A(A(tests_OK_group_⋅,tests_OK_group_e),$5_0) -> $5_0,
+A(A(tests_OK_group_⋅,$6_0),tests_OK_group_e) -> $6_0,
+A(A(tests_OK_group_⋅,A(tests_OK_group_inv,$7_0)),$7_0) -> tests_OK_group_e,
+A(A(tests_OK_group_⋅,$8_0),A(tests_OK_group_inv,$8_0)) -> tests_OK_group_e,
 A(A(tests_OK_group_⋅,A(tests_OK_group_inv,$9_0)),A(A(tests_OK_group_⋅,$9_0),$9_1)) -> $9_1,
 A(A(tests_OK_group_⋅,$10_0),A(A(tests_OK_group_⋅,A(tests_OK_group_inv,$10_0)),$10_1)) -> $10_1
 )
diff --git a/tests/regressions/xtc.expected b/tests/regressions/xtc.expected
index dfe72a5d4..a33544fd5 100644
--- a/tests/regressions/xtc.expected
+++ b/tests/regressions/xtc.expected
@@ -5,10 +5,10 @@
     <rules>
       <rule>
         <lhs>
-          <funapp><name>tests.OK.group.inv</name><arg><funapp><name>tests.OK.group.1</name></funapp></arg></funapp>
+          <funapp><name>tests.OK.group.inv</name><arg><funapp><name>tests.OK.group.e</name></funapp></arg></funapp>
         </lhs>
         <rhs>
-          <funapp><name>tests.OK.group.1</name></funapp>
+          <funapp><name>tests.OK.group.e</name></funapp>
         </rhs>
       </rule>
       <rule>
@@ -37,7 +37,7 @@
       </rule>
       <rule>
         <lhs>
-          <funapp><name>tests.OK.group.⋅</name><arg><funapp><name>tests.OK.group.1</name></funapp></arg><arg><var>5_0</var></arg></funapp>
+          <funapp><name>tests.OK.group.⋅</name><arg><funapp><name>tests.OK.group.e</name></funapp></arg><arg><var>5_0</var></arg></funapp>
         </lhs>
         <rhs>
           <var>5_0</var>
@@ -45,7 +45,7 @@
       </rule>
       <rule>
         <lhs>
-          <funapp><name>tests.OK.group.⋅</name><arg><var>6_0</var></arg><arg><funapp><name>tests.OK.group.1</name></funapp></arg></funapp>
+          <funapp><name>tests.OK.group.⋅</name><arg><var>6_0</var></arg><arg><funapp><name>tests.OK.group.e</name></funapp></arg></funapp>
         </lhs>
         <rhs>
           <var>6_0</var>
@@ -56,7 +56,7 @@
           <funapp><name>tests.OK.group.⋅</name><arg><funapp><name>tests.OK.group.inv</name><arg><var>7_0</var></arg></funapp></arg><arg><var>7_0</var></arg></funapp>
         </lhs>
         <rhs>
-          <funapp><name>tests.OK.group.1</name></funapp>
+          <funapp><name>tests.OK.group.e</name></funapp>
         </rhs>
       </rule>
       <rule>
@@ -64,7 +64,7 @@
           <funapp><name>tests.OK.group.⋅</name><arg><var>8_0</var></arg><arg><funapp><name>tests.OK.group.inv</name><arg><var>8_0</var></arg></funapp></arg></funapp>
         </lhs>
         <rhs>
-          <funapp><name>tests.OK.group.1</name></funapp>
+          <funapp><name>tests.OK.group.e</name></funapp>
         </rhs>
       </rule>
       <rule>
@@ -145,7 +145,7 @@
       </variableTypeInfo>
       <functionSymbolTypeInfo>
         <funcDeclaration>
-          <name>tests.OK.group.1</name>
+          <name>tests.OK.group.e</name>
           <typeDeclaration><type><basic>tests.OK.group.G</basic></type></typeDeclaration>
         </funcDeclaration>
         <funcDeclaration>

From 13fe4126f945f7736248239bfda06cf01cb4013e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Fri, 24 Jan 2025 21:53:20 +0100
Subject: [PATCH 2/9] wip

---
 .github/workflows/main.yml | 23 +++++++++++++----------
 1 file changed, 13 insertions(+), 10 deletions(-)

diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
index f616cf8d8..832aa7331 100644
--- a/.github/workflows/main.yml
+++ b/.github/workflows/main.yml
@@ -4,22 +4,23 @@ on:
   push:
   workflow_dispatch:
 jobs:
-  build_lambdapi:
+  lambdapi:
     strategy:
       fail-fast: false
       matrix:
+        os: [ubuntu-latest, macos-latest, windows-latest]
         ocaml-version: [5.3.0, 5.2.1, 5.1.1, 5.0.0, 4.14.2, 4.13.1, 4.12.1, 4.11.2, 4.10.2, 4.09.1]
-    runs-on: ubuntu-latest
+    runs-on: ${{ matrix.os }}-latest
     steps:
       - name: checking out lambdapi repo ...
         uses: actions/checkout@v4
-      - name: recovering cached opam files ...
-        uses: actions/cache@v4
-        with:
-          path: ~/.opam
-          key: ${{ runner.os }}-ocaml-${{ matrix.ocaml-version }}
+      # - name: recovering cached opam files ...
+      #   uses: actions/cache@v4
+      #   with:
+      #     path: ~/.opam
+      #     key: ${{ runner.os }}-ocaml-${{ matrix.ocaml-version }}
       - name: setting up opam ...
-        uses: avsm/setup-ocaml@v3
+        uses: ocaml/setup-ocaml@v3
         with:
           ocaml-compiler: ${{ matrix.ocaml-version }}
       - name: installing dependencies ...
@@ -34,10 +35,12 @@ jobs:
           eval $(opam env)
           #why3 config detect
           make tests
-  build_vscode_extension:
+  vscode_extension:
     strategy:
       fail-fast: false
-    runs-on: ubuntu-latest
+      matrix:
+        os: [ubuntu-latest, macos-latest, windows-latest]
+    runs-on: ${{ matrix.os }}
     steps:
       - name: checking out lambdapi repo ...
         uses: actions/checkout@v4

From 99a5034db42875181c2c7589583242961a06ef88 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Fri, 24 Jan 2025 22:06:29 +0100
Subject: [PATCH 3/9] wip

---
 .github/workflows/main.yml | 29 +++++++++++++++++++++++++++--
 1 file changed, 27 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
index 832aa7331..bb0107b30 100644
--- a/.github/workflows/main.yml
+++ b/.github/workflows/main.yml
@@ -8,7 +8,7 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        os: [ubuntu-latest, macos-latest, windows-latest]
+        os: [ubuntu-latest] #, macos-latest, windows-latest]
         ocaml-version: [5.3.0, 5.2.1, 5.1.1, 5.0.0, 4.14.2, 4.13.1, 4.12.1, 4.11.2, 4.10.2, 4.09.1]
     runs-on: ${{ matrix.os }}-latest
     steps:
@@ -39,7 +39,7 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        os: [ubuntu-latest, macos-latest, windows-latest]
+        os: [ubuntu-latest] #, macos-latest, windows-latest]
     runs-on: ${{ matrix.os }}
     steps:
       - name: checking out lambdapi repo ...
@@ -61,3 +61,28 @@ jobs:
         with: 
           name: assets-for-download
           path: editors/vscode/extensionFolder
+  # lint-fmt:
+  #   runs-on: ubuntu-latest
+  #   steps:
+  #     - name: Checkout tree
+  #       uses: actions/checkout@v4
+  #     - name: Set-up OCaml
+  #       uses: ocaml/setup-ocaml@v3
+  #       with:
+  #         ocaml-compiler: 5
+  #     - uses: ocaml/setup-ocaml/lint-fmt@v3
+  lint-opam:
+    strategy:
+      fail-fast: false
+      matrix:
+        os: [ubuntu-latest] #, macos-latest, windows-latest]
+        ocaml-version: [5.3.0, 5.2.1, 5.1.1, 5.0.0, 4.14.2, 4.13.1, 4.12.1, 4.11.2, 4.10.2, 4.09.1]
+    runs-on: ${{ matrix.os }}-latest
+    steps:
+      - name: Checkout tree
+        uses: actions/checkout@v4
+      - name: Set-up OCaml
+        uses: ocaml/setup-ocaml@v3
+        with:
+          ocaml-compiler: ${{ matrix.ocaml-version }}
+      - uses: ocaml/setup-ocaml/lint-opam@v3

From 83f61c5f9c1965984a29664ea2b35cbe982b98eb Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Fri, 24 Jan 2025 22:09:38 +0100
Subject: [PATCH 4/9] wip

---
 .github/workflows/main.yml | 9 ++-------
 1 file changed, 2 insertions(+), 7 deletions(-)

diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
index bb0107b30..c3059c1a9 100644
--- a/.github/workflows/main.yml
+++ b/.github/workflows/main.yml
@@ -72,17 +72,12 @@ jobs:
   #         ocaml-compiler: 5
   #     - uses: ocaml/setup-ocaml/lint-fmt@v3
   lint-opam:
-    strategy:
-      fail-fast: false
-      matrix:
-        os: [ubuntu-latest] #, macos-latest, windows-latest]
-        ocaml-version: [5.3.0, 5.2.1, 5.1.1, 5.0.0, 4.14.2, 4.13.1, 4.12.1, 4.11.2, 4.10.2, 4.09.1]
-    runs-on: ${{ matrix.os }}-latest
+    runs-on: ubuntu-latest
     steps:
       - name: Checkout tree
         uses: actions/checkout@v4
       - name: Set-up OCaml
         uses: ocaml/setup-ocaml@v3
         with:
-          ocaml-compiler: ${{ matrix.ocaml-version }}
+          ocaml-compiler: 5
       - uses: ocaml/setup-ocaml/lint-opam@v3

From ff7b7ade6993b6a550e526fccc1bbd5e684eaf26 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Fri, 24 Jan 2025 23:00:31 +0100
Subject: [PATCH 5/9] wip

---
 .github/workflows/main.yml | 20 ++++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
index c3059c1a9..87ba8d4a8 100644
--- a/.github/workflows/main.yml
+++ b/.github/workflows/main.yml
@@ -71,13 +71,13 @@ jobs:
   #       with:
   #         ocaml-compiler: 5
   #     - uses: ocaml/setup-ocaml/lint-fmt@v3
-  lint-opam:
-    runs-on: ubuntu-latest
-    steps:
-      - name: Checkout tree
-        uses: actions/checkout@v4
-      - name: Set-up OCaml
-        uses: ocaml/setup-ocaml@v3
-        with:
-          ocaml-compiler: 5
-      - uses: ocaml/setup-ocaml/lint-opam@v3
+  # lint-opam:
+  #   runs-on: ubuntu-latest
+  #   steps:
+  #     - name: Checkout tree
+  #       uses: actions/checkout@v4
+  #     - name: Set-up OCaml
+  #       uses: ocaml/setup-ocaml@v3
+  #       with:
+  #         ocaml-compiler: 5
+  #     - uses: ocaml/setup-ocaml/lint-opam@v3

From c364791b3017db21edc549057e42822731755f6e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Sat, 25 Jan 2025 08:28:00 +0100
Subject: [PATCH 6/9] update doc

---
 doc/README.md    |  8 +++++---
 doc/lambdapi.bnf | 37 +++++++++++++------------------------
 2 files changed, 18 insertions(+), 27 deletions(-)

diff --git a/doc/README.md b/doc/README.md
index 4669eb5eb..590fa8be4 100644
--- a/doc/README.md
+++ b/doc/README.md
@@ -21,9 +21,11 @@ The Lamdbapi user manual can also be generated from the sources and browsed loca
 browser.
 
 To generate the documentation, [Sphinx](https://www.sphinx-doc.org/)
-and `sphinx_rtd_theme` are required.  They can be installed using
-`pip` as follows:
-
+and `sphinx_rtd_theme` are required. They can be globally installed with:
+```bash
+sudo apt install python3-sphinx-rtd-theme
+```
+and locally with:
 ```bash
 sudo apt install python3-pip
 pip install -U sphinx sphinx_rtd_theme
diff --git a/doc/lambdapi.bnf b/doc/lambdapi.bnf
index 546461b7a..eb133f684 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_int> ";"
+<command> ::= "opaque" <qid> ";"
             | "require" "open" <path>* ";"
             | "require" <path>* ";"
             | "require" <path> "as" <uid> ";"
             | "open" <path>* ";"
-            | <modifier>* "symbol" <uid_or_int> <param_list>* ":" <term>
-              [<proof>] ";"
-            | <modifier>* "symbol" <uid_or_int> <param_list>* [":" <term>]
-              "≔" <term_proof> ";"
+            | <modifier>* "symbol" <uid> <param_list>* ":" <term> [<proof>]
+              ";"
+            | <modifier>* "symbol" <uid> <param_list>* [":" <term>] "≔"
+              <term_proof> ";"
             | [<exposition>] <param_list>* "inductive" <inductive> ("with"
               <inductive>)* ";"
             | "rule" <rule> ("with" <rule>)* ";"
-            | "builtin" <stringlit> "≔" <qid_or_int> ";"
+            | "builtin" <stringlit> "≔" <qid> ";"
             | "coerce_rule" <rule> ";"
             | "unif_rule" <unif_rule> ";"
-            | "notation" <qid_or_int> <notation> ";"
+            | "notation" <qid> <notation> ";"
             | <query> ";"
             
 
@@ -45,8 +45,8 @@ QID ::= [UID "."]+ UID
           | "debug" ("+"|"-") <string>
           | "flag" <stringlit> <switch>
           | "prover" <stringlit>
-          | "prover_timeout" <nat>
-          | "verbose" <nat>
+          | "prover_timeout" "in"T
+          | "verbose" "in"T
           | "type" <term>
           | "search" <stringlit>
 
@@ -70,18 +70,11 @@ QID ::= [UID "."]+ UID
 
 <uid> ::= UID
 
-<uid_or_int> ::= <uid>
-               | <int>
-
-<qid_or_int> ::= <qid>
-               | <int>
-
 <param_list> ::= <param>
                | "(" <param>+ ":" <term> ")"
                | "[" <param>+ [":" <term>] "]"
 
 <param> ::= <uid>
-          | <nat>
           | "_"
 
 <term> ::= <bterm>
@@ -103,8 +96,7 @@ QID ::= [UID "."]+ UID
           | "$" UID [<env>]
           | "(" <term> ")"
           | "[" <term> "]"
-          | <nat>
-          | "-"<nat>
+          | "in"T
 
 <env> ::= "." "[" [<term> (";" <term>)*] "]"
 
@@ -152,7 +144,7 @@ QID ::= [UID "."]+ UID
            | "reflexivity"
            | "remove" <uid>+
            | "rewrite" [<side>] [<rw_patt_spec>] <term>
-           | "simplify" [<qid_or_int>]
+           | "simplify" [<qid>]
            | "solve"
            | "symmetry"
            | "try" <tactic>
@@ -169,7 +161,7 @@ QID ::= [UID "."]+ UID
 <inductive> ::= <uid> <param_list>* ":" <term> "≔" ["|"] [<constructor>
                 ("|" <constructor>)*]
 
-<constructor> ::= <uid_or_int> <param_list>* ":" <term>
+<constructor> ::= <uid> <param_list>* ":" <term>
 
 <rule> ::= <term> "↪" <term>
 
@@ -184,10 +176,7 @@ QID ::= [UID "."]+ UID
              | "quantifier"
 
 <float_or_int> ::= <float>
-                 | <int>
-
-<int> ::= "-"<nat>
-        | <nat>
+                 | "in"T
 
 <maybe_generalize> ::= ["generalize"]
 

From 0229b5c8bb495bbbdee5252d6cd831c41fbdeb0c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Sat, 25 Jan 2025 09:47:39 +0100
Subject: [PATCH 7/9] wip

---
 doc/commands.rst                   | 56 ++++++++++++++++--------------
 doc/terms.rst                      | 17 ++++++++-
 src/core/print.ml                  | 50 ++++++++++++++++++--------
 src/core/sign.ml                   | 16 +++++++--
 src/handle/command.ml              | 12 +++++++
 src/parsing/pratt.ml               |  2 +-
 tests/OK/print_notation_numbers.lp | 41 ++++++++++++++++++++++
 7 files changed, 149 insertions(+), 45 deletions(-)
 create mode 100644 tests/OK/print_notation_numbers.lp

diff --git a/doc/commands.rst b/doc/commands.rst
index 3ee401f3c..1a313eac6 100644
--- a/doc/commands.rst
+++ b/doc/commands.rst
@@ -206,11 +206,10 @@ commands :ref:`notation` and :ref:`builtin`.
 
 The ``notation`` command allows to change the behaviour of the parser.
 
-When declared as notations, identifiers then must be used at correct places
-and as such cannot make valid terms on their own anymore.
-To reaccess the value of the identifier without the notation properties,
-wrap it in parentheses.
-
+When declared as notations, identifiers must be used at correct places
+and are not valid terms on their own anymore.  To reaccess the value
+of the identifier without the notation properties, wrap it in
+parentheses like in ``(+)`` if ``+`` is declared ``infix``.
 
 **infix** The following code defines infix symbols for addition
 and multiplication. Both are associative to the left, and they have
@@ -251,7 +250,6 @@ negation with some priority level.
 * The functional arrow has a lower binding power than any operator, therefore
   for any prefix operator ``-``, ``- A → A`` is always parsed ``(- A) → A``
 
-
 **quantifier** Allows to write ```f x, t`` instead of ``f (λ x, t)``:
 
 ::
@@ -262,6 +260,31 @@ negation with some priority level.
    type λ p, `∀ x, p; // quantifiers can be written as such
    type λ p, `f x, p; // works as well if f is any symbol
 
+**printing numbers in decimal notation** It is possible to print various number types in decimal notation by defining the following builtins:
+
+* Natural numbers in base 1 (Peano numbers):
+
+::
+   
+   builtin "nat_zero" ≔ ...; // : N
+   builtin "nat_succ" ≔ ...; // : N → N
+
+* Positive natural numbers in base 2:
+
+::
+   
+   builtin "pos_one" ≔ ...; // : P
+   builtin "pos_double" ≔ ...; // : P → P
+   builtin "pos_succ_double" ≔ ...; // : P → P
+
+* Integer numbers in base 2:
+
+::
+   
+   builtin "int_zero" ≔ ...; // : Z
+   builtin "int_positive" ≔ ...; // : P → Z
+   builtin "int_negative" ≔ ...; // : P → Z
+
 .. _builtin:
 
 ``builtin``
@@ -269,26 +292,7 @@ negation with some priority level.
 
 The command ``builtin`` allows to map a “builtin“
 string to a user-defined symbol identifier. Those mappings are
-necessary for other commands or tactics. For instance, to use decimal
-numbers, one needs to map the builtins “0“ and “+1“ to some symbol
-identifiers for zero and the successor function (see hereafter); to
-use tactics on equality, one needs to define some specific builtins;
-etc.
-
-**decimal notation for integers** It is possible to use the standard
-decimal notation for integers by defining the builtins ``"0"`` to
-``"10"``, ``"+"``, ``"*"``, and ``"-"`` (optional):
-
-::
-
-   builtin "0"  ≔ ...;  // : N
-   builtin "1"  ≔ ...;  // : N
-   ...
-   builtin "10" := ...; // : N
-   builtin "+" := ....; // : N → N → N
-   builtin "*" := ....; // : N → N → N
-   builtin "-" := ....; // : N → N // (optional)
-   type 42;
+necessary for other commands, tactics or notations to work.
 
 .. _opaque:
 
diff --git a/doc/terms.rst b/doc/terms.rst
index 71b1efce9..be4b65d44 100644
--- a/doc/terms.rst
+++ b/doc/terms.rst
@@ -77,9 +77,24 @@ A user-defined term can be either:
   variable in a rule left-hand side, applied to all the variables of
   the context.
 
-* an integer if the appropriate :ref:`builtins <builtin>` are defined
+* an integer if the appropriate builtins are defined (see below)
 
 * a term enclosed between square brackets ``[`` … ``]`` for explicitly
   giving the value of an argument declared as implicit
   
 Subterms can be parenthesized to avoid ambiguities.
+
+**decimal notation for integers** It is possible to use the standard
+decimal notation for integers by defining the following :ref:`builtins
+<builtin>`:
+
+::
+
+   builtin "0"  ≔ ...;  // : T
+   builtin "1"  ≔ ...;  // : T
+   ...
+   builtin "10" := ...; // : T
+   builtin "+" := ....; // : T → T → T
+   builtin "*" := ....; // : T → T → T
+   builtin "-" := ....; // : T → T // (optional)
+   type 42;
diff --git a/src/core/print.ml b/src/core/print.ml
index ed05cde22..17bd36c66 100644
--- a/src/core/print.ml
+++ b/src/core/print.ml
@@ -50,10 +50,9 @@ let notation : 'a pp -> 'a Sign.notation pp = fun elt ->
   | Sign.Prefix(p) -> out ppf "prefix %a" elt p
   | Infix(a,p) -> out ppf "infix%a %a" assoc a elt p
   | Postfix(p) -> out ppf "postfix %a" elt p
-  | Zero -> ()
-  | Succ None -> ()
   | Succ (Some n) -> notation ppf n
   | Quant -> out ppf "quantifier"
+  | _ -> ()
   in notation
 
 let uid : string pp = string
@@ -108,19 +107,13 @@ let var : 'a Bindlib.var pp = fun ppf x -> uid ppf (Bindlib.name_of x)
 
 (** Exception raised when trying to convert a term into a nat. *)
 exception Not_a_nat
+let builtin name =
+  try StrMap.find name (!sig_state).builtins with Not_found -> raise Not_a_nat
 
 (** [nat_of_term t] converts a term into a natural number.
     @raise Not_a_nat if this is not possible. *)
 let nat_of_term : term -> int = fun t ->
-  let get_builtin name =
-    try StrMap.find name (!sig_state).builtins
-    with Not_found -> raise Not_a_nat
-  in
-  let zero = get_builtin "0" in
-  match get_args t with
-  | (Symb s, []) when s == zero -> 0
-  | _ ->
-  let succ = get_builtin "+1" in
+  let zero = builtin "nat_zero" and succ = builtin "nat_succ" in
   let rec nat acc = fun t ->
     match get_args t with
     | (Symb s, [u]) when s == succ -> nat (acc+1) u
@@ -128,6 +121,30 @@ let nat_of_term : term -> int = fun t ->
     | _ -> raise Not_a_nat
   in nat 0 t
 
+(** [pos_of_term t] converts a term into a positive number.
+    @raise Not_a_nat if this is not possible. *)
+let pos_of_term : term -> int = fun t ->
+  let one = builtin "pos_one" and dbl = builtin "pos_double"
+  and suc_dbl = builtin "pos_succ_double" in
+  let rec pos acc = fun t ->
+    match get_args t with
+    | (Symb s, [u]) when s == dbl -> pos (2*acc) u
+    | (Symb s, [u]) when s == suc_dbl -> pos (2*acc+1) u
+    | (Symb s,  []) when s == one -> acc
+    | _ -> raise Not_a_nat
+  in pos 1 t
+
+(** [int_of_term t] converts a term into a positive number.
+    @raise Not_a_nat if this is not possible. *)
+let int_of_term : term -> int = fun t ->
+  let zero = builtin "int_zero" and pos = builtin "int_positive"
+  and neg = builtin "int_negative" in
+  match get_args t with
+  | (Symb s, [u]) when s == pos -> pos_of_term u
+  | (Symb s, [u]) when s == neg -> - (pos_of_term u)
+  | (Symb s,  []) when s == zero -> 0
+  | _ -> raise Not_a_nat
+
 (** [are_quant_args args] returns [true] iff [args] has only one argument
    that is an abstraction. *)
 let are_quant_args : term list -> bool = fun args ->
@@ -181,6 +198,8 @@ and term : term pp = fun ppf t ->
     | Symb(s) ->
         if !print_implicits && s.sym_impl <> [] then pp_appl h args
         else
+          let number f t =
+            try out ppf "%i" (f t) with Not_a_nat -> pp_appl h args in
           let args = LibTerm.remove_impl_args s args in
           begin match notation_of s with
           | Some Quant when are_quant_args args ->
@@ -207,13 +226,14 @@ and term : term pp = fun ppf t ->
                   List.iter (out ppf " %a" atom) args;
                   if p = `Atom then out ppf ")"
               end
-          | Some Zero -> out ppf "0"
+          | Some (Zero|IntZero) -> out ppf "0"
           | Some (Succ (Some (Postfix _))) ->
               (try out ppf "%i" (nat_of_term t)
                with Not_a_nat -> postfix h s args)
-          | Some (Succ _) ->
-              (try out ppf "%i" (nat_of_term t)
-               with Not_a_nat -> pp_appl h args)
+          | Some (Succ _) -> number nat_of_term t
+          | Some PosOne -> out ppf "1"
+          | Some (PosDouble|PosSuccDouble) -> number pos_of_term t
+          | Some (IntPos|IntNeg) -> number int_of_term t
           | _ -> pp_appl h args
           end
     | _ -> pp_appl h args
diff --git a/src/core/sign.ml b/src/core/sign.ml
index 584d3515c..7c1eddb06 100644
--- a/src/core/sign.ml
+++ b/src/core/sign.ml
@@ -24,6 +24,12 @@ type 'a notation =
   | Zero
   | Succ of 'a notation option (* Prefix or Postfix only *)
   | Quant
+  | PosOne
+  | PosDouble
+  | PosSuccDouble
+  | IntZero
+  | IntPos
+  | IntNeg
 
 (** Representation of a signature. It roughly corresponds to a set of symbols,
     defined in a single module (or file). *)
@@ -368,8 +374,14 @@ let add_notation_from_builtin :
   string -> sym -> 'a notation SymMap.t -> 'a notation SymMap.t =
   fun builtin sym notation_map ->
   match builtin with
-  | "0"  -> SymMap.add sym Zero notation_map
-  | "+1" -> let f x = Some(Succ x) in SymMap.update sym f notation_map
+  | "nat_zero"  -> SymMap.add sym Zero notation_map
+  | "nat_succ" -> let f x = Some(Succ x) in SymMap.update sym f notation_map
+  | "pos_one"  -> SymMap.add sym PosOne notation_map
+  | "pos_double"  -> SymMap.add sym PosDouble notation_map
+  | "pos_succ_double"  -> SymMap.add sym PosSuccDouble notation_map
+  | "int_zero"  -> SymMap.add sym IntZero notation_map
+  | "int_positive"  -> SymMap.add sym IntPos notation_map
+  | "int_negative"  -> SymMap.add sym IntNeg notation_map
   | _    -> notation_map
 
 (** [add_builtin sign name sym] binds the builtin name [name] to [sym] (in the
diff --git a/src/handle/command.ml b/src/handle/command.ml
index a9c820deb..fae357494 100644
--- a/src/handle/command.ml
+++ b/src/handle/command.ml
@@ -265,6 +265,12 @@ let get_proof_data : compiler -> sig_state -> p_command -> cmd_output =
         | Zero -> 0
         | Succ _ -> 1
         | Quant -> 1
+        | PosOne -> 0
+        | PosDouble -> 1
+        | PosSuccDouble -> 1
+        | IntZero -> 0
+        | IntPos -> 1
+        | IntNeg -> 1
       and real = Tactic.count_products [] !(s.sym_type) in
       if real < expected then
         fatal pos "Notation incompatible with the type of %a" sym s;
@@ -283,6 +289,12 @@ let get_proof_data : compiler -> sig_state -> p_command -> cmd_output =
         | Succ x -> Succ (Option.map float_notation_from_string_notation x)
         | Zero -> Zero
         | Quant -> Quant
+        | PosOne -> PosOne
+        | PosDouble -> PosDouble
+        | PosSuccDouble -> PosSuccDouble
+        | IntZero -> IntZero
+        | IntPos -> IntPos
+        | IntNeg -> IntNeg
       in
       let n = float_notation_from_string_notation n in
       Console.out 2 "notation %a %a" sym s (notation float) n;
diff --git a/src/parsing/pratt.ml b/src/parsing/pratt.ml
index 70b67e2ce..3b27a5fc4 100644
--- a/src/parsing/pratt.ml
+++ b/src/parsing/pratt.ml
@@ -40,7 +40,7 @@ end = struct
              Some(Pratter.Prefix, prio)
          | Some(Postfix(prio)) | Some(Succ(Some(Postfix(prio)))) ->
              Some(Pratter.Postfix, prio)
-         | Some (Zero | Succ _ | Quant) | None -> None)
+         | _ -> None)
      | _ -> None
 
    let appl : p_term -> p_term -> p_term = fun t u ->
diff --git a/tests/OK/print_notation_numbers.lp b/tests/OK/print_notation_numbers.lp
new file mode 100644
index 000000000..c15067ffb
--- /dev/null
+++ b/tests/OK/print_notation_numbers.lp
@@ -0,0 +1,41 @@
+symbol N:TYPE;
+symbol z:N;
+symbol s:N → N;
+
+builtin "nat_zero" ≔ z;
+builtin "nat_succ" ≔ s;
+
+compute s(s z);
+
+symbol P:TYPE;
+symbol H:P;
+symbol O:P → P;
+symbol I:P → P;
+
+builtin "pos_one" ≔ H;
+builtin "pos_double" ≔ O;
+builtin "pos_succ_double" ≔ I;
+
+compute I(O(I H));
+
+symbol double:N → N;
+rule double z ↪ z
+with double (s $x) ↪ s(s(double $x));
+
+symbol val:P → N;
+rule val H ↪ s z
+with val (O $x) ↪ double(val $x)
+with val (I $x) ↪ s(double(val $x));
+
+compute val(I(O(I H)));
+
+symbol Z:TYPE;
+symbol Z0:Z;
+symbol Zpos:P → Z;
+symbol Zneg:P → Z;
+
+builtin "int_zero" ≔ Z0;
+builtin "int_positive" ≔ Zpos;
+builtin "int_negative" ≔ Zneg;
+
+compute Zneg(I(O(I H)));

From af64a38f92a09d524c9dfe0c3e5a534c234c8829 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Sat, 25 Jan 2025 10:00:09 +0100
Subject: [PATCH 8/9] wip

---
 .github/workflows/main.yml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
index 87ba8d4a8..7442fdac8 100644
--- a/.github/workflows/main.yml
+++ b/.github/workflows/main.yml
@@ -10,7 +10,7 @@ jobs:
       matrix:
         os: [ubuntu-latest] #, macos-latest, windows-latest]
         ocaml-version: [5.3.0, 5.2.1, 5.1.1, 5.0.0, 4.14.2, 4.13.1, 4.12.1, 4.11.2, 4.10.2, 4.09.1]
-    runs-on: ${{ matrix.os }}-latest
+    runs-on: ${{ matrix.os }}
     steps:
       - name: checking out lambdapi repo ...
         uses: actions/checkout@v4
@@ -35,7 +35,7 @@ jobs:
           eval $(opam env)
           #why3 config detect
           make tests
-  vscode_extension:
+  vscode:
     strategy:
       fail-fast: false
       matrix:

From 0c5e04414a41527d2efdaec8ea7ab2a3be8f1d2f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Sat, 25 Jan 2025 10:07:35 +0100
Subject: [PATCH 9/9] wip

---
 .github/workflows/main.yml | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
index 7442fdac8..418e93527 100644
--- a/.github/workflows/main.yml
+++ b/.github/workflows/main.yml
@@ -8,9 +8,8 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        os: [ubuntu-latest] #, macos-latest, windows-latest]
         ocaml-version: [5.3.0, 5.2.1, 5.1.1, 5.0.0, 4.14.2, 4.13.1, 4.12.1, 4.11.2, 4.10.2, 4.09.1]
-    runs-on: ${{ matrix.os }}
+    runs-on: ubuntu-latest
     steps:
       - name: checking out lambdapi repo ...
         uses: actions/checkout@v4
@@ -38,9 +37,7 @@ jobs:
   vscode:
     strategy:
       fail-fast: false
-      matrix:
-        os: [ubuntu-latest] #, macos-latest, windows-latest]
-    runs-on: ${{ matrix.os }}
+    runs-on: ubuntu-latest
     steps:
       - name: checking out lambdapi repo ...
         uses: actions/checkout@v4