new theorems added. does not comile well yet :(( problems found in

[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / Level-1 / LambdaDelta / T / defs.ma

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs.ma
index cf483de06c4a16a6dd2868497a150cd74195d7a8..cc5d917318e05b9643df31f4b1fbf3686fe934d6 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs.ma
@@ -36,18 +36,10 @@ inductive T: Set \def
 | TLRef: nat \to T
 | THead: K \to (T \to (T \to T)).
 
-inductive TList: Set \def
-| TNil: TList
-| TCons: T \to (TList \to TList).
-
-definition THeads:
- K \to (TList \to (T \to T))
+definition tweight:
+ T \to nat
 \def
- let rec THeads (k: K) (us: TList) on us: (T \to T) \def (\lambda (t: 
-T).(match us with [TNil \Rightarrow t | (TCons u ul) \Rightarrow (THead k u 
-(THeads k ul t))])) in THeads.
-
-inductive C: Set \def
-| CSort: nat \to C
-| CHead: C \to (K \to (T \to C)).
+ let rec tweight (t: T) on t: nat \def (match t with [(TSort _) \Rightarrow 
+(S O) | (TLRef _) \Rightarrow (S O) | (THead _ u t0) \Rightarrow (S (plus 
+(tweight u) (tweight t0)))]) in tweight.