X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2FC%2Fdefs.ma;h=9d41d8ce5a9c3eabd5893a9d9eab4f8cf431a490;hb=57ae1762497a5f3ea75740e2908e04adb8642cc2;hp=2f08ba725e3253df99f625ec29e6b1fdac87999b;hpb=639e798161afea770f41d78673c0fe3be4125beb;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_1/C/defs.ma b/matita/matita/contribs/lambdadelta/basic_1/C/defs.ma
index 2f08ba725..9d41d8ce5 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/C/defs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/C/defs.ma
@@ -20,8 +20,8 @@ inductive C: Type[0] \def
 | CSort: nat \to C
 | CHead: C \to (K \to (T \to C)).
 
-let rec cweight (c: C) on c: nat \def match c with [(CSort _) \Rightarrow O | 
-(CHead c0 _ t) \Rightarrow (plus (cweight c0) (tweight t))].
+rec definition cweight (c: C) on c: nat \def match c with [(CSort _) 
+\Rightarrow O | (CHead c0 _ t) \Rightarrow (plus (cweight c0) (tweight t))].
 
 definition clt:
  C \to (C \to Prop)
@@ -33,7 +33,7 @@ definition cle:
 \def
  \lambda (c1: C).(\lambda (c2: C).(le (cweight c1) (cweight c2))).
 
-let rec CTail (k: K) (t: T) (c: C) on c: C \def match c with [(CSort n) 
-\Rightarrow (CHead (CSort n) k t) | (CHead d h u) \Rightarrow (CHead (CTail k 
-t d) h u)].
+rec definition CTail (k: K) (t: T) (c: C) on c: C \def match c with [(CSort 
+n) \Rightarrow (CHead (CSort n) k t) | (CHead d h u) \Rightarrow (CHead 
+(CTail k t d) h u)].