From 03e705fa7bb3246db35d144ae4e47946d9782a34 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 8 Jun 2005 16:32:50 +0000
Subject: [PATCH] Using the lighter syntax for "let recs".

---
 helm/matita/tests/match.ma | 27 ++++++++-------------------
 1 file changed, 8 insertions(+), 19 deletions(-)

diff --git a/helm/matita/tests/match.ma b/helm/matita/tests/match.ma
index 9494d9cc8..c952d0a92 100644
--- a/helm/matita/tests/match.ma
+++ b/helm/matita/tests/match.ma
@@ -97,13 +97,10 @@ intros.elim n.apply O_S.apply not_eq_S.assumption.
 qed.
 
 
-definition plus : nat \to nat \to nat \def
-let rec plus n m \def 
+let rec plus n m : nat \def 
  match n with 
  [ O \Rightarrow m
- | (S p) \Rightarrow S (plus p m) ]
-in
-plus.
+ | (S p) \Rightarrow S (plus p m) ].
 
 theorem plus_n_O: \forall n:nat. eq nat n (plus n O).
 intros.elim n.simplify.apply refl_equal.simplify.apply f_equal.assumption.
@@ -123,13 +120,10 @@ theorem assoc_plus:
 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 : nat \def 
  match n with 
  [ O \Rightarrow O
- | (S p) \Rightarrow (plus m (times p m)) ]
-in
-times.
+ | (S p) \Rightarrow (plus m (times p m)) ].
 
 theorem times_n_O: \forall n:nat. eq nat O (times n O).
 intros.elim n.simplify.apply refl_equal.simplify.assumption.
@@ -151,16 +145,13 @@ intros.elim n.simplify.apply times_n_O.
 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 : nat \def 
  [\lambda n:nat.nat] match n with 
  [ O \Rightarrow O
  | (S p) \Rightarrow 
 	[\lambda n:nat.nat] match m with
 	[O \Rightarrow (S p)
-        | (S q) \Rightarrow minus p q ]]
-in
-minus.
+        | (S q) \Rightarrow minus p q ]].
 
 theorem nat_case :
 \forall n:nat.\forall P:nat \to Prop. 
@@ -270,15 +261,13 @@ apply le_S_n.assumption.
 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 : bool \def 
    [\lambda n:nat.bool] match n with 
     [ O \Rightarrow true
     | (S p) \Rightarrow
 	[\lambda n:nat.bool] match m with 
         [ O \Rightarrow false
-	| (S q) \Rightarrow leb p q]]
-in leb.
+	| (S q) \Rightarrow leb p q]].
 
 theorem le_dec: \forall n,m:nat. if_then_else (leb n m) (le n m) (Not (le n m)).
 intros.
-- 
2.39.2