X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2Ftlt_defs.ma;h=390c067cc15823721e09fdf7f81653f2f1e2a9c1;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=f2bf3660d561341ff17e08f4d4b977e223cc635a;hpb=2ff23d9306837c14c9d1a3b935a66bc71ffe87c3;p=helm.git

diff --git a/helm/matita/contribs/LAMBDA-TYPES/tlt_defs.ma b/helm/matita/contribs/LAMBDA-TYPES/tlt_defs.ma
index f2bf3660d..390c067cc 100644
--- a/helm/matita/contribs/LAMBDA-TYPES/tlt_defs.ma
+++ b/helm/matita/contribs/LAMBDA-TYPES/tlt_defs.ma
@@ -23,29 +23,31 @@ definition wadd: (nat \to nat) \to nat \to (nat \to nat) \def
       | (S m) \Rightarrow (map m)
    ].
 
-let rec weight_map (A:Set) (N:Set) (map:nat \to nat) (t:T) : nat \def 
+let rec weight_map (A:Set) (N:Set) (map:nat \to nat) (t:T A N) on t : nat \def 
    match t with [
-        (TSort A N y k)     \Rightarrow O
-      | (TLRef A N y i)     \Rightarrow (map i)
-      | (TWag A N y z w u) \Rightarrow
+        (TSort y k)     \Rightarrow O
+      | (TLRef y i)     \Rightarrow (map i)
+      | (TWag y z w u) \Rightarrow
          match z with [
               (Bind b) \Rightarrow
                  match b with [
                       Abbr \Rightarrow
-                        (S (plus (weight_map A N map w) (weight_map A N (wadd map (S (weight_map A N map w))) u)))
+                        (S ((weight_map A N map w) + (weight_map A N (wadd map (S (weight_map A N map w))) u)))
                     | Abst \Rightarrow 
-                        (S (plus (weight_map A N map w) (weight_map A N (wadd map O) u)))
+                        (S ((weight_map A N map w) + (weight_map A N (wadd map O) u)))
                     | Void \Rightarrow 
-                        (S (plus (weight_map A N map w) (weight_map A N (wadd map O) u)))
+                        (S ((weight_map A N map w) + (weight_map A N (wadd map O) u)))
                  ]
             | (Flat a) \Rightarrow
-                 (S (plus (weight_map A N map w) (weight_map A N map u)))
-         ]].(*
-      | (TGRef A N y n)     \Rightarrow O
-  ].*)
-(*
-      Definition weight : T \to nat := (weight_map [_](0)).
+                 (S ((weight_map A N map w) + (weight_map A N map u)))
+         ]
+      | (TGRef y n)     \Rightarrow O
+  ].
 
-      Definition tlt : T \to T \to Prop := [t1,t2](lt (weight t1) (weight t2)).
+definition weight: \forall A,N. T A N \to nat \def 
+   \lambda A,N. 
+   (weight_map A N (\lambda _.O)).
 
-*)
+definition tlt: \forall A,N. T A N \to T A N \to Prop \def 
+   \lambda A,N,t1,t2. 
+   weight A N t1 < weight A N t2.