Added aliases and notation.

diff --git a/helm/matita/contribs/LAMBDA-TYPES/lref_map_defs.ma b/helm/matita/contribs/LAMBDA-TYPES/lref_map_defs.ma
index f2994f9b79b5185b4250e5ff11bc5956b703fbf0..572618808d33101ac9bbcd6e1de7c45c533009e8 100644 (file)
--- a/helm/matita/contribs/LAMBDA-TYPES/lref_map_defs.ma
+++ b/helm/matita/contribs/LAMBDA-TYPES/lref_map_defs.ma
@@ -18,5 +18,5 @@ include "terms_defs.ma".
 
 inductive tlref_map (A: Set) (N: Set) (map: nat \to nat): nat \to (T A N) \to (T A N) \to Prop \def
    | tlref_map_sort: \forall i. \forall k. \forall y. (tlref_map A N map i (TSort A N y k) (TSort A N y k))
-   | tlref_map_lref_lt: \forall j. \forall i. \forall y. (lt j i) \to (tlref_map A N map i (TLRef A N y j) (TLRef A N y j))
-   | tlref_map_lref_ge: \forall j. \forall i. \forall y. (le i j) \to (tlref_map A N map i (TLRef A N y j) (TLRef A N y (map j))).
\ No newline at end of file
+   | tlref_map_lref_lt: \forall j. \forall i. \forall y. j < i \to (tlref_map A N map i (TLRef A N y j) (TLRef A N y j))
+   | tlref_map_lref_ge: \forall j. \forall i. \forall y. i \le j \to (tlref_map A N map i (TLRef A N y j) (TLRef A N y (map j))).

diff --git a/helm/matita/contribs/LAMBDA-TYPES/terms_defs.ma b/helm/matita/contribs/LAMBDA-TYPES/terms_defs.ma
index 6a88b1da30a40c2523e564b50b4135ed9c3e2012..9a2c5fb9d2ebd1df4704a47dbbfcc5ab701c511b 100644 (file)
--- a/helm/matita/contribs/LAMBDA-TYPES/terms_defs.ma
+++ b/helm/matita/contribs/LAMBDA-TYPES/terms_defs.ma
@@ -14,6 +14,15 @@
 
 set "baseuri" "cic:/matita/LAMBDA-TYPES/terms_defs".
 
+include "coq.ma".
+
+alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
+alias id "S" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)".
+alias id "O" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)".
+alias id "plus" = "cic:/Coq/Init/Peano/plus.con".
+alias id "lt" = "cic:/Coq/Init/Peano/lt.con".
+alias id "le" = "cic:/Coq/Init/Peano/le.ind#xpointer(1/1)".
+
 inductive B : Set \def 
    | Void: B
    | Abbr: B
@@ -27,7 +36,6 @@ inductive W : Set \def
    | Bind: B \to W 
    | Flat: F \to W.
 
-alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
 inductive T (A:Set) (N:Set) : Set \def
    | TSort: A \to nat \to (T A N) 
    | TLRef: A \to nat \to (T A N)

diff --git a/helm/matita/contribs/LAMBDA-TYPES/tlt_defs.ma b/helm/matita/contribs/LAMBDA-TYPES/tlt_defs.ma
index 09ae56ef8d64ab3e9332b3790bc3e21eecc89897..1d5f73f17b01283028da43a233572ae7e6c6bb46 100644 (file)
--- a/helm/matita/contribs/LAMBDA-TYPES/tlt_defs.ma
+++ b/helm/matita/contribs/LAMBDA-TYPES/tlt_defs.ma
@@ -32,18 +32,18 @@ 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 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. \lambda t1,t2. weight A N t1 < weight A N t2.