tests/OK/natural.lp: add builtins for printing Peano numbers in decim…

…al notation (#1186)

src/core/print.ml

@@ -107,6 +107,7 @@ 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
 

tests/OK/natural.lp

@@ -27,7 +27,7 @@ with (s $m) × $n     ↪ $n + $m × $n
 with _      × z      ↪ z
 with $m     × (s $n) ↪ $m + $m × $n;
 
-// Enabling decimal notation
+// Enabling parsing of decimal notation
 
 symbol n1 ≔ s z;
 symbol n2 ≔ s n1;
@@ -57,14 +57,19 @@ 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;
 
+// Enabling printing of decimal notation
+
+builtin "nat_zero" ≔ z;
+builtin "nat_succ" ≔ s;
+
+compute 4 + 5;
+
 // Doubling function.
 
 symbol double n ≔ n × 2;

tests/OK/perf_rw_fib-nonRightLin.lp

@@ -13,4 +13,4 @@ with fib3 (s (s (s $x))) ↪ (fib3 ($x + 2)) + (fib3 ($x + 1)) + (fib3 $x);
 
 assert ⊢ fib 15 ≡ 610;
 compute fib 24; // ≡ 46368;
-compute fib3 21;
+//compute fib3 21;