Typing errors fixed.

diff --git a/helm/matita/contribs/LAMBDA-TYPES/tlt_defs.ma b/helm/matita/contribs/LAMBDA-TYPES/tlt_defs.ma
index f2bf3660d561341ff17e08f4d4b977e223cc635a..09ae56ef8d64ab3e9332b3790bc3e21eecc89897 100644 (file)
--- a/helm/matita/contribs/LAMBDA-TYPES/tlt_defs.ma
+++ b/helm/matita/contribs/LAMBDA-TYPES/tlt_defs.ma
@@ -23,11 +23,11 @@ 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 [
@@ -40,12 +40,10 @@ let rec weight_map (A:Set) (N:Set) (map:nat \to nat) (t:T) : nat \def
                  ]
             | (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)).
+         ]
+      | (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. \lambda t1,t2. (lt (weight A N t1) (weight A N t2)).
\ No newline at end of file