From f2f6b3b567d556e732a8ae861ea633b0804840fb Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 8 Jun 2005 16:31:02 +0000
Subject: [PATCH] Using the top-level syntax for let-rec definitions.

---
 helm/matita/tests/letrec.ma | 14 +++++++-------
 helm/matita/tests/match.ma  |  8 ++++----
 2 files changed, 11 insertions(+), 11 deletions(-)

diff --git a/helm/matita/tests/letrec.ma b/helm/matita/tests/letrec.ma
index 6712765aa..464f7fa21 100644
--- a/helm/matita/tests/letrec.ma
+++ b/helm/matita/tests/letrec.ma
@@ -1,9 +1,9 @@
 
-definition plus: nat \to nat \to nat \def
-  let rec plus (n,m:nat) \def
-    match n with
-    [ O \Rightarrow m
-    | (S x) \Rightarrow S (plus x m) ]
-  in
-  plus.
+alias id "O" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)".
+alias id "S" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)".
+alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
 
+let rec plus n m : nat \def
+ match n with
+  [ O \Rightarrow m
+  | (S x) \Rightarrow S (plus x m) ].
diff --git a/helm/matita/tests/match.ma b/helm/matita/tests/match.ma
index 2382ba7b7..9494d9cc8 100644
--- a/helm/matita/tests/match.ma
+++ b/helm/matita/tests/match.ma
@@ -98,7 +98,7 @@ qed.
 
 
 definition plus : nat \to nat \to nat \def
-let rec plus (n,m) \def 
+let rec plus n m \def 
  match n with 
  [ O \Rightarrow m
  | (S p) \Rightarrow S (plus p m) ]
@@ -124,7 +124,7 @@ intros.elim n.simplify.apply refl_equal.simplify.apply f_equal.assumption.
 qed.
 
 definition times : nat \to nat \to nat \def
-let rec times (n,m) \def 
+let rec times n m \def 
  match n with 
  [ O \Rightarrow O
  | (S p) \Rightarrow (plus m (times p m)) ]
@@ -152,7 +152,7 @@ simplify.elim (sym_eq ? ? ? H).apply times_n_Sm.
 qed.
 
 definition minus : nat \to nat \to nat \def
-let rec minus (n,m) \def 
+let rec minus n m \def 
  [\lambda n:nat.nat] match n with 
  [ O \Rightarrow O
  | (S p) \Rightarrow 
@@ -271,7 +271,7 @@ apply le_S_n.assumption.
 qed.
 
 definition leb : nat \to nat \to bool \def
-let rec leb (n,m) \def 
+let rec leb n m \def 
    [\lambda n:nat.bool] match n with 
     [ O \Rightarrow true
     | (S p) \Rightarrow
-- 
2.39.2