From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 5 Sep 2005 12:04:50 +0000 (+0000)
Subject: Typing errors fixed.
X-Git-Tag: V_0_1_2_1~106
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ded933cd70fc158d915d6aff3bfc6f775fe09333;p=helm.git

Typing errors fixed.
---

diff --git a/helm/matita/contribs/LAMBDA-TYPES/tlt_defs.ma b/helm/matita/contribs/LAMBDA-TYPES/tlt_defs.ma
index f2bf3660d..09ae56ef8 100644
--- 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