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

diff --git a/helm/matita/contribs/LAMBDA-TYPES/tlt_defs.ma b/helm/matita/contribs/LAMBDA-TYPES/tlt_defs.ma
index 09ae56ef8..390c067cc 100644
--- a/helm/matita/contribs/LAMBDA-TYPES/tlt_defs.ma
+++ b/helm/matita/contribs/LAMBDA-TYPES/tlt_defs.ma
@@ -32,18 +32,22 @@ let rec weight_map (A:Set) (N:Set) (map:nat \to nat) (t:T A N) on t : nat \def
               (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)))
+                 (S ((weight_map A N map w) + (weight_map A N map u)))
          ]
       | (TGRef y n)     \Rightarrow O
   ].
 
-definition weight : \forall A,N. T A N \to nat \def \lambda A,N.(weight_map A N (\lambda _.O)).
+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
+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.