From 1e7db0c9a71cb3720d36ab090706a84e3f539fe0 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 5 Sep 2005 17:14:12 +0000 Subject: [PATCH] Added aliases and notation. --- helm/matita/contribs/LAMBDA-TYPES/lref_map_defs.ma | 4 ++-- helm/matita/contribs/LAMBDA-TYPES/terms_defs.ma | 10 +++++++++- helm/matita/contribs/LAMBDA-TYPES/tlt_defs.ma | 10 +++++----- 3 files changed, 16 insertions(+), 8 deletions(-) diff --git a/helm/matita/contribs/LAMBDA-TYPES/lref_map_defs.ma b/helm/matita/contribs/LAMBDA-TYPES/lref_map_defs.ma index f2994f9b7..572618808 100644 --- 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 6a88b1da3..9a2c5fb9d 100644 --- 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 09ae56ef8..1d5f73f17 100644 --- 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. -- 2.39.2