From 82299c3f801926c85a89c98185501fc780e92fa2 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 15 Sep 2006 14:14:17 +0000 Subject: [PATCH] useless files removed --- matita/contribs/LAMBDA-TYPES/lref_map_defs.ma | 22 -------- matita/contribs/LAMBDA-TYPES/makefile | 33 ------------ matita/contribs/LAMBDA-TYPES/terms_defs.ma | 47 ---------------- matita/contribs/LAMBDA-TYPES/tlt_defs.ma | 53 ------------------- 4 files changed, 155 deletions(-) delete mode 100644 matita/contribs/LAMBDA-TYPES/lref_map_defs.ma delete mode 100644 matita/contribs/LAMBDA-TYPES/makefile delete mode 100644 matita/contribs/LAMBDA-TYPES/terms_defs.ma delete mode 100644 matita/contribs/LAMBDA-TYPES/tlt_defs.ma diff --git a/matita/contribs/LAMBDA-TYPES/lref_map_defs.ma b/matita/contribs/LAMBDA-TYPES/lref_map_defs.ma deleted file mode 100644 index 572618808..000000000 --- a/matita/contribs/LAMBDA-TYPES/lref_map_defs.ma +++ /dev/null @@ -1,22 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -set "baseuri" "cic:/matita/LAMBDA-TYPES/lref_map_defs". - -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. 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/matita/contribs/LAMBDA-TYPES/makefile b/matita/contribs/LAMBDA-TYPES/makefile deleted file mode 100644 index 9ef6694ee..000000000 --- a/matita/contribs/LAMBDA-TYPES/makefile +++ /dev/null @@ -1,33 +0,0 @@ -H=@ - -RT_BASEDIR=../../ -OPTIONS=-bench -MMAKE=$(RT_BASEDIR)matitamake $(OPTIONS) -CLEAN=$(RT_BASEDIR)matitaclean $(OPTIONS) -MMAKEO=$(RT_BASEDIR)matitamake.opt $(OPTIONS) -CLEANO=$(RT_BASEDIR)matitaclean.opt $(OPTIONS) - -devel:=$(shell basename `pwd`) - -all: preall - $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) build $(devel) -clean: preall - $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) clean $(devel) -cleanall: preall - $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MCLEAN) all - -all.opt opt: preall - $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) build $(devel) -clean.opt: preall - $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) clean $(devel) -cleanall.opt: preall - $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MCLEANO) all - -%.mo: preall - $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) $@ -%.mo.opt: preall - $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) $@ - -preall: - $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) init $(devel) - diff --git a/matita/contribs/LAMBDA-TYPES/terms_defs.ma b/matita/contribs/LAMBDA-TYPES/terms_defs.ma deleted file mode 100644 index cf7848abe..000000000 --- a/matita/contribs/LAMBDA-TYPES/terms_defs.ma +++ /dev/null @@ -1,47 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -set "baseuri" "cic:/matita/LAMBDA-TYPES/terms_defs". - -include "legacy/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 - | Abst: B. - -inductive F : Set \def - | Appl: F - | Cast: F. - -inductive W : Set \def - | Bind: B \to W - | Flat: F \to W. - -inductive T (A:Set) (N:Set) : Set \def - | TSort: A \to nat \to (T A N) - | TLRef: A \to nat \to (T A N) - | TWag : A \to W \to (T A N) \to (T A N) \to (T A N) - | TGRef: A \to N \to (T A N). - -record X (A:Set) (N:Set) : Type \def { - get_gref: N \to B \to (T A N) \to Prop -}. diff --git a/matita/contribs/LAMBDA-TYPES/tlt_defs.ma b/matita/contribs/LAMBDA-TYPES/tlt_defs.ma deleted file mode 100644 index 390c067cc..000000000 --- a/matita/contribs/LAMBDA-TYPES/tlt_defs.ma +++ /dev/null @@ -1,53 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -set "baseuri" "cic:/matita/LAMBDA-TYPES/tlt_defs". - -include "terms_defs.ma". - -definition wadd: (nat \to nat) \to nat \to (nat \to nat) \def - \lambda map,w,n. - match n with [ - O \Rightarrow w - | (S m) \Rightarrow (map m) - ]. - -let rec weight_map (A:Set) (N:Set) (map:nat \to nat) (t:T A N) on t : nat \def - match t with [ - (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 [ - Abbr \Rightarrow - (S ((weight_map A N map w) + (weight_map A N (wadd map (S (weight_map A N map w))) u))) - | Abst \Rightarrow - (S ((weight_map A N map w) + (weight_map A N (wadd map O) u))) - | Void \Rightarrow - (S ((weight_map A N map w) + (weight_map A N (wadd map O) u))) - ] - | (Flat a) \Rightarrow - (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,t1,t2. - weight A N t1 < weight A N t2. -- 2.39.2