X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLevel-1%2FLambdaDelta%2FT%2Fdefs.ma;h=5db7814395963a8d6ed448877342094142e967ea;hb=bfb39a9bcb10b87ab7d6e09928fb82d340d8feca;hp=42d3dcb191a94b838db0d6cf5a2269bd87e29491;hpb=7dba28380b550e8a1b34d3282afd3329df7055cc;p=helm.git

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 42d3dcb19..5db781439 100644
--- 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
@@ -47,3 +47,10 @@ definition THeads:
 T).(match us with [TNil \Rightarrow t | (TCons u ul) \Rightarrow (THead k u 
 (THeads k ul t))])) in THeads.
 
+definition tweight:
+ T \to nat
+\def
+ 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.
+