legacy_1, ground_1, and basic_1 recommitted without anticipation

[helm.git] / matita / matita / contribs / lambdadelta / basic_1 / C / defs.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_1/C/defs.ma b/matita/matita/contribs/lambdadelta/basic_1/C/defs.ma
index cecc082677e494c409001a1d93ced6ff865642f1..2f08ba725e3253df99f625ec29e6b1fdac87999b 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_1/C/defs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/C/defs.ma
@@ -14,17 +14,14 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Basic-1/T/defs.ma".
+include "basic_1/T/defs.ma".
 
-inductive C: Set \def
+inductive C: Type[0] \def
 | CSort: nat \to C
 | CHead: C \to (K \to (T \to C)).
 
-definition cweight:
- C \to nat
-\def
- let rec cweight (c: C) on c: nat \def (match c with [(CSort _) \Rightarrow O 
-| (CHead c0 _ t) \Rightarrow (plus (cweight c0) (tweight t))]) in cweight.
+let rec 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)
@@ -36,10 +33,7 @@ definition cle:
 \def
  \lambda (c1: C).(\lambda (c2: C).(le (cweight c1) (cweight c2))).
 
-definition CTail:
- K \to (T \to (C \to C))
-\def
- let rec CTail (k: K) (t: T) (c: C) on c: C \def (match c with [(CSort n) 
+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)]) in CTail.
+t d) h u)].