From ec897a47d5c194a068ee76f9251958950371876b Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 7 Jun 2011 21:37:47 +0000 Subject: [PATCH] - we removed the reduction-related item categorization - some renaming --- matita/matita/lib/lambda-delta/notation.ma | 12 ------------ .../lib/lambda-delta/substitution/lift.ma | 2 +- .../lib/lambda-delta/substitution/subst.ma | 2 +- .../lambda-delta/{language => syntax}/item.ma | 17 ----------------- .../lambda-delta/{language => syntax}/lenv.ma | 2 +- .../lib/lambda-delta/{language => syntax}/sh.ma | 0 .../lambda-delta/{language => syntax}/term.ma | 2 +- .../lambda-delta/{language => syntax}/weight.ma | 2 +- 8 files changed, 5 insertions(+), 34 deletions(-) rename matita/matita/lib/lambda-delta/{language => syntax}/item.ma (70%) rename matita/matita/lib/lambda-delta/{language => syntax}/lenv.ma (95%) rename matita/matita/lib/lambda-delta/{language => syntax}/sh.ma (100%) rename matita/matita/lib/lambda-delta/{language => syntax}/term.ma (96%) rename matita/matita/lib/lambda-delta/{language => syntax}/weight.ma (96%) diff --git a/matita/matita/lib/lambda-delta/notation.ma b/matita/matita/lib/lambda-delta/notation.ma index 7f5fabf28..09960abe3 100644 --- a/matita/matita/lib/lambda-delta/notation.ma +++ b/matita/matita/lib/lambda-delta/notation.ma @@ -13,18 +13,6 @@ (* language *****************************************************************) -notation "hvbox( ζ I )" - non associative with precedence 45 - for @{ 'Zeta $I }. - -notation "hvbox( τ I )" - non associative with precedence 45 - for @{ 'Tau $I }. - -notation "hvbox( θ I )" - non associative with precedence 45 - for @{ 'Theta $I }. - notation "hvbox( ⋆ )" non associative with precedence 90 for @{ 'Star }. diff --git a/matita/matita/lib/lambda-delta/substitution/lift.ma b/matita/matita/lib/lambda-delta/substitution/lift.ma index 656946171..6b97f502c 100644 --- a/matita/matita/lib/lambda-delta/substitution/lift.ma +++ b/matita/matita/lib/lambda-delta/substitution/lift.ma @@ -9,7 +9,7 @@ \ / V_______________________________________________________________ *) -include "lambda-delta/language/term.ma". +include "lambda-delta/syntax/term.ma". (* RELOCATION ***************************************************************) diff --git a/matita/matita/lib/lambda-delta/substitution/subst.ma b/matita/matita/lib/lambda-delta/substitution/subst.ma index 5989693c5..a9732529d 100644 --- a/matita/matita/lib/lambda-delta/substitution/subst.ma +++ b/matita/matita/lib/lambda-delta/substitution/subst.ma @@ -9,7 +9,7 @@ \ / V_______________________________________________________________ *) -include "lambda-delta/language/lenv.ma". +include "lambda-delta/syntax/lenv.ma". include "lambda-delta/substitution/lift.ma". (* TELESCOPIC SUBSTITUTION **************************************************) diff --git a/matita/matita/lib/lambda-delta/language/item.ma b/matita/matita/lib/lambda-delta/syntax/item.ma similarity index 70% rename from matita/matita/lib/lambda-delta/language/item.ma rename to matita/matita/lib/lambda-delta/syntax/item.ma index 60a115dc0..742ff2272 100644 --- a/matita/matita/lib/lambda-delta/language/item.ma +++ b/matita/matita/lib/lambda-delta/syntax/item.ma @@ -40,20 +40,3 @@ inductive item2: Type[0] ≝ coercion item2_of_bind2: ∀I:bind2.item2 ≝ Bind on _I:bind2 to item2. coercion item2_of_flat2: ∀I:flat2.item2 ≝ Flat on _I:flat2 to item2. - -(* reduction-related categorization *****************************************) - -(* binding items entitled for zeta-reduction *) -definition zable ≝ λI. I = Abbr. - -interpretation "is entitled for zeta-reduction" 'Zeta I = (zable I). - -(* non-binding items entitled for zeta-reduction *) -definition table ≝ λI. I = Cast. - -interpretation "is entitled for tau-reduction" 'Tau I = (table I). - -(* binding items entitled for theta-reduction *) -definition thable ≝ λI. I = Abbr. - -interpretation "is entitled for theta-reduction" 'Theta I = (thable I). diff --git a/matita/matita/lib/lambda-delta/language/lenv.ma b/matita/matita/lib/lambda-delta/syntax/lenv.ma similarity index 95% rename from matita/matita/lib/lambda-delta/language/lenv.ma rename to matita/matita/lib/lambda-delta/syntax/lenv.ma index 3398de4ee..c3aab910b 100644 --- a/matita/matita/lib/lambda-delta/language/lenv.ma +++ b/matita/matita/lib/lambda-delta/syntax/lenv.ma @@ -9,7 +9,7 @@ \ / V_______________________________________________________________ *) -include "lambda-delta/language/term.ma". +include "lambda-delta/syntax/term.ma". (* LOCAL ENVIRONMENTS *******************************************************) diff --git a/matita/matita/lib/lambda-delta/language/sh.ma b/matita/matita/lib/lambda-delta/syntax/sh.ma similarity index 100% rename from matita/matita/lib/lambda-delta/language/sh.ma rename to matita/matita/lib/lambda-delta/syntax/sh.ma diff --git a/matita/matita/lib/lambda-delta/language/term.ma b/matita/matita/lib/lambda-delta/syntax/term.ma similarity index 96% rename from matita/matita/lib/lambda-delta/language/term.ma rename to matita/matita/lib/lambda-delta/syntax/term.ma index ac3b8fa5e..fe84e54b4 100644 --- a/matita/matita/lib/lambda-delta/language/term.ma +++ b/matita/matita/lib/lambda-delta/syntax/term.ma @@ -9,7 +9,7 @@ \ / V_______________________________________________________________ *) -include "lambda-delta/language/item.ma". +include "lambda-delta/syntax/item.ma". (* TERMS ********************************************************************) diff --git a/matita/matita/lib/lambda-delta/language/weight.ma b/matita/matita/lib/lambda-delta/syntax/weight.ma similarity index 96% rename from matita/matita/lib/lambda-delta/language/weight.ma rename to matita/matita/lib/lambda-delta/syntax/weight.ma index f0021be9e..8d5ed6835 100644 --- a/matita/matita/lib/lambda-delta/language/weight.ma +++ b/matita/matita/lib/lambda-delta/syntax/weight.ma @@ -9,7 +9,7 @@ \ / V_______________________________________________________________ *) -include "lambda-delta/language/lenv.ma". +include "lambda-delta/syntax/lenv.ma". (* WEIGHTS ******************************************************************) -- 2.39.2