From: Ferruccio Guidi Date: Thu, 18 Aug 2011 22:07:11 +0000 (+0000) Subject: - some refactoring X-Git-Tag: make_still_working~2332 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fd991956035d0f1b663aab48325097e53ed9e00e;p=helm.git - some refactoring - we fixed some wrong preambles in the scripts --- diff --git a/matita/matita/contribs/lambda-delta/Basic-2/grammar/item.ma b/matita/matita/contribs/lambda-delta/Basic-2/grammar/item.ma new file mode 100644 index 000000000..3db6ebf53 --- /dev/null +++ b/matita/matita/contribs/lambda-delta/Basic-2/grammar/item.ma @@ -0,0 +1,46 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* THE FORMAL SYSTEM λδ - MATITA SOURCE SCRIPTS + * Specification started: 2011 April 17 + * - Patience on me so that I gain peace and perfection! - + * [ suggested invocation to start formal specifications with ] + *) + +include "Ground-2/ground.ma". +include "Basic-2/notation.ma". + +(* BINARY ITEMS *************************************************************) + +(* binary binding items *) +inductive bind2: Type[0] ≝ +| Abbr: bind2 (* abbreviation *) +| Abst: bind2 (* abstraction *) +. + +(* binary non-binding items *) +inductive flat2: Type[0] ≝ +| Appl: flat2 (* application *) +| Cast: flat2 (* explicit type annotation *) +. + +(* binary items *) +inductive item2: Type[0] ≝ +| Bind: bind2 → item2 (* binding item *) +| Flat: flat2 → item2 (* non-binding item *) +. + +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. diff --git a/matita/matita/contribs/lambda-delta/Basic-2/grammar/lenv.ma b/matita/matita/contribs/lambda-delta/Basic-2/grammar/lenv.ma new file mode 100644 index 000000000..ad903c9d1 --- /dev/null +++ b/matita/matita/contribs/lambda-delta/Basic-2/grammar/lenv.ma @@ -0,0 +1,27 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +include "Basic-2/grammar/term.ma". + +(* LOCAL ENVIRONMENTS *******************************************************) + +(* local environments *) +inductive lenv: Type[0] ≝ +| LSort: lenv (* empty *) +| LPair: lenv → bind2 → term → lenv (* binary binding construction *) +. + +interpretation "sort (local environment)" 'Star = LSort. + +interpretation "environment binding construction (binary)" 'DBind L I T = (LPair L I T). diff --git a/matita/matita/contribs/lambda-delta/Basic-2/grammar/lenv_length.ma b/matita/matita/contribs/lambda-delta/Basic-2/grammar/lenv_length.ma new file mode 100644 index 000000000..437730a83 --- /dev/null +++ b/matita/matita/contribs/lambda-delta/Basic-2/grammar/lenv_length.ma @@ -0,0 +1,25 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +include "Basic-2/grammar/lenv.ma". + +(* LENGTH *******************************************************************) + +(* the length of a local environment *) +let rec length L ≝ match L with +[ LSort ⇒ 0 +| LPair L _ _ ⇒ length L + 1 +]. + +interpretation "length (local environment)" 'card L = (length L). diff --git a/matita/matita/contribs/lambda-delta/Basic-2/grammar/lenv_weight.ma b/matita/matita/contribs/lambda-delta/Basic-2/grammar/lenv_weight.ma new file mode 100644 index 000000000..1d918d3a8 --- /dev/null +++ b/matita/matita/contribs/lambda-delta/Basic-2/grammar/lenv_weight.ma @@ -0,0 +1,35 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +include "Basic-2/grammar/term_weight.ma". +include "Basic-2/grammar/lenv.ma". + +(* WEIGHTS ******************************************************************) + +(* the weight of a local environment *) +let rec lw L ≝ match L with +[ LSort ⇒ 0 +| LPair L _ V ⇒ lw L + #V +]. + +interpretation "weight (local environment)" 'Weight L = (lw L). + +(* the weight of a closure *) +definition cw: lenv → term → ? ≝ λL,T. #L + #T. + +interpretation "weight (closure)" 'Weight L T = (cw L T). + +axiom cw_wf_ind: ∀P:lenv→term→Prop. + (∀L2,T2. (∀L1,T1. #[L1,T1] < #[L2,T2] → P L1 T1) → P L2 T2) → + ∀L,T. P L T. diff --git a/matita/matita/contribs/lambda-delta/Basic-2/grammar/sh.ma b/matita/matita/contribs/lambda-delta/Basic-2/grammar/sh.ma new file mode 100644 index 000000000..e6188a882 --- /dev/null +++ b/matita/matita/contribs/lambda-delta/Basic-2/grammar/sh.ma @@ -0,0 +1,23 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +include "Ground-2/ground.ma". + +(* SORT HIERARCHY ***********************************************************) + +(* sort hierarchy specifications *) +record sh: Type[0] ≝ { + next: nat → nat; (* next sort in the hierarchy *) + next_lt: ∀k. k < next k (* strict monotonicity condition *) +}. diff --git a/matita/matita/contribs/lambda-delta/Basic-2/grammar/term.ma b/matita/matita/contribs/lambda-delta/Basic-2/grammar/term.ma new file mode 100644 index 000000000..2cd284655 --- /dev/null +++ b/matita/matita/contribs/lambda-delta/Basic-2/grammar/term.ma @@ -0,0 +1,34 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +include "Basic-2/grammar/item.ma". + +(* TERMS ********************************************************************) + +(* terms *) +inductive term: Type[0] ≝ +| TSort: nat → term (* sort: starting at 0 *) +| TLRef: nat → term (* reference by index: starting at 0 *) +| TPair: item2 → term → term → term (* binary item construction *) +. + +interpretation "sort (term)" 'Star k = (TSort k). + +interpretation "local reference (term)" 'Weight i = (TLRef i). + +interpretation "term construction (binary)" 'SItem I T1 T2 = (TPair I T1 T2). + +interpretation "term binding construction (binary)" 'SBind I T1 T2 = (TPair (Bind I) T1 T2). + +interpretation "term flat construction (binary)" 'SFlat I T1 T2 = (TPair (Flat I) T1 T2). diff --git a/matita/matita/contribs/lambda-delta/Basic-2/grammar/term_weight.ma b/matita/matita/contribs/lambda-delta/Basic-2/grammar/term_weight.ma new file mode 100644 index 000000000..5d880eb6e --- /dev/null +++ b/matita/matita/contribs/lambda-delta/Basic-2/grammar/term_weight.ma @@ -0,0 +1,30 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +include "Basic-2/grammar/term.ma". + +(* WEIGHT *******************************************************************) + +(* the weight of a term *) +let rec tw T ≝ match T with +[ TSort _ ⇒ 1 +| TLRef _ ⇒ 1 +| TPair _ V T ⇒ tw V + tw T + 1 +]. + +interpretation "weight (term)" 'Weight T = (tw T). + +axiom tw_wf_ind: ∀P:term→Prop. + (∀T2. (∀T1. # T1 < # T2 → P T1) → P T2) → + ∀T. P T. diff --git a/matita/matita/contribs/lambda-delta/Basic-2/notation.ma b/matita/matita/contribs/lambda-delta/Basic-2/notation.ma index 375d06abc..d4302a32a 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/notation.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/notation.ma @@ -1,17 +1,20 @@ -(* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department of the University of Bologna, Italy. - ||I|| - ||T|| - ||A|| This file is distributed under the terms of the - \ / GNU General Public License Version 2 - \ / - V_______________________________________________________________ *) +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -(* Syntax *******************************************************************) +(* Grammar ******************************************************************) notation "hvbox( ⋆ )" non associative with precedence 90 diff --git a/matita/matita/contribs/lambda-delta/Basic-2/reduction/cpr.ma b/matita/matita/contribs/lambda-delta/Basic-2/reduction/cpr.ma index 878e27048..21169192c 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/reduction/cpr.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/reduction/cpr.ma @@ -1,13 +1,16 @@ -(* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department of the University of Bologna, Italy. - ||I|| - ||T|| - ||A|| This file is distributed under the terms of the - \ / GNU General Public License Version 2 - \ / - V_______________________________________________________________ *) +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) include "Basic-2/reduction/tpr.ma". diff --git a/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr.ma b/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr.ma index 54564f796..42d4b4e94 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr.ma @@ -1,13 +1,16 @@ -(* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department of the University of Bologna, Italy. - ||I|| - ||T|| - ||A|| This file is distributed under the terms of the - \ / GNU General Public License Version 2 - \ / - V_______________________________________________________________ *) +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) include "Basic-2/substitution/tps.ma". diff --git a/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_tpr.ma b/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_tpr.ma index 140eeb334..aec243d13 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_tpr.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_tpr.ma @@ -1,15 +1,17 @@ -(* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department of the University of Bologna, Italy. - ||I|| - ||T|| - ||A|| This file is distributed under the terms of the - \ / GNU General Public License Version 2 - \ / - V_______________________________________________________________ *) +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) -include "Basic-2/substitution/lift_weight.ma". include "Basic-2/substitution/tps_tps.ma". include "Basic-2/reduction/tpr_lift.ma". include "Basic-2/reduction/tpr_tps.ma". diff --git a/matita/matita/contribs/lambda-delta/Basic-2/substitution/drop.ma b/matita/matita/contribs/lambda-delta/Basic-2/substitution/drop.ma index dccc186e1..f9219f27f 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/substitution/drop.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/substitution/drop.ma @@ -1,13 +1,16 @@ -(* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department of the University of Bologna, Italy. - ||I|| - ||T|| - ||A|| This file is distributed under the terms of the - \ / GNU General Public License Version 2 - \ / - V_______________________________________________________________ *) +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) include "Basic-2/substitution/leq.ma". include "Basic-2/substitution/lift.ma". diff --git a/matita/matita/contribs/lambda-delta/Basic-2/substitution/leq.ma b/matita/matita/contribs/lambda-delta/Basic-2/substitution/leq.ma index e843982cd..7f5c12e01 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/substitution/leq.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/substitution/leq.ma @@ -1,15 +1,18 @@ -(* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department of the University of Bologna, Italy. - ||I|| - ||T|| - ||A|| This file is distributed under the terms of the - \ / GNU General Public License Version 2 - \ / - V_______________________________________________________________ *) +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) -include "Basic-2/syntax/length.ma". +include "Basic-2/grammar/lenv_length.ma". (* LOCAL ENVIRONMENT EQUALITY ***********************************************) diff --git a/matita/matita/contribs/lambda-delta/Basic-2/substitution/lift.ma b/matita/matita/contribs/lambda-delta/Basic-2/substitution/lift.ma index c6ec4033f..7526f0c45 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/substitution/lift.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/substitution/lift.ma @@ -1,15 +1,18 @@ -(* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department of the University of Bologna, Italy. - ||I|| - ||T|| - ||A|| This file is distributed under the terms of the - \ / GNU General Public License Version 2 - \ / - V_______________________________________________________________ *) - -include "Basic-2/syntax/term.ma". +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +include "Basic-2/grammar/term_weight.ma". (* RELOCATION ***************************************************************) @@ -72,6 +75,12 @@ lemma lift_split: ∀d1,e2,T1,T2. ↑[d1, e2] T1 ≡ T2 → ∀d2,e1. ] qed. +(* Basic forward lemmas *****************************************************) + +lemma tw_lift: ∀d,e,T1,T2. ↑[d, e] T1 ≡ T2 → #T1 = #T2. +#d #e #T1 #T2 #H elim H -d e T1 T2; normalize // +qed. + (* Basic inversion lemmas ***************************************************) lemma lift_inv_refl_aux: ∀d,e,T1,T2. ↑[d, e] T1 ≡ T2 → e = 0 → T1 = T2. diff --git a/matita/matita/contribs/lambda-delta/Basic-2/substitution/lift_weight.ma b/matita/matita/contribs/lambda-delta/Basic-2/substitution/lift_weight.ma deleted file mode 100644 index 84c8fef1d..000000000 --- a/matita/matita/contribs/lambda-delta/Basic-2/substitution/lift_weight.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 *) -(* *) -(**************************************************************************) - -include "Basic-2/syntax/weight.ma". -include "Basic-2/substitution/lift.ma". - -(* RELOCATION ***************************************************************) - -lemma tw_lift: ∀d,e,T1,T2. ↑[d, e] T1 ≡ T2 → #T1 = #T2. -#d #e #T1 #T2 #H elim H -d e T1 T2; normalize // -qed. diff --git a/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps.ma b/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps.ma index cf20a0056..d2c9e636b 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps.ma @@ -1,13 +1,16 @@ -(* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department of the University of Bologna, Italy. - ||I|| - ||T|| - ||A|| This file is distributed under the terms of the - \ / GNU General Public License Version 2 - \ / - V_______________________________________________________________ *) +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) include "Basic-2/substitution/drop.ma". diff --git a/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps_lift.ma b/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps_lift.ma index 06d102945..98c73149d 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps_lift.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps_lift.ma @@ -1,13 +1,16 @@ -(* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department of the University of Bologna, Italy. - ||I|| - ||T|| - ||A|| This file is distributed under the terms of the - \ / GNU General Public License Version 2 - \ / - V_______________________________________________________________ *) +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) include "Basic-2/substitution/drop_drop.ma". include "Basic-2/substitution/tps.ma". diff --git a/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps_split.ma b/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps_split.ma index 8d093e46b..041bb0c98 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps_split.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps_split.ma @@ -1,13 +1,16 @@ -(* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department of the University of Bologna, Italy. - ||I|| - ||T|| - ||A|| This file is distributed under the terms of the - \ / GNU General Public License Version 2 - \ / - V_______________________________________________________________ *) +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) include "Basic-2/substitution/tps_lift.ma". diff --git a/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps_tps.ma b/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps_tps.ma index 7143620d1..857bc7ebe 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps_tps.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps_tps.ma @@ -1,13 +1,16 @@ -(* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department of the University of Bologna, Italy. - ||I|| - ||T|| - ||A|| This file is distributed under the terms of the - \ / GNU General Public License Version 2 - \ / - V_______________________________________________________________ *) +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) include "Basic-2/substitution/tps_split.ma". diff --git a/matita/matita/contribs/lambda-delta/Ground-2/ground.ma b/matita/matita/contribs/lambda-delta/Ground-2/ground.ma index bf266c347..11b2a8d92 100644 --- a/matita/matita/contribs/lambda-delta/Ground-2/ground.ma +++ b/matita/matita/contribs/lambda-delta/Ground-2/ground.ma @@ -1,13 +1,16 @@ -(* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department of the University of Bologna, Italy. - ||I|| - ||T|| - ||A|| This file is distributed under the terms of the - \ / GNU General Public License Version 2 - \ / - V_______________________________________________________________ *) +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) include "arithmetics/nat.ma". include "Ground-2/xoa_props.ma".