From a5548736278a0b63f6f25c2721934ed8a7d2eef8 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 21 Oct 2015 17:05:02 +0000 Subject: [PATCH] parked material ... --- .../lenv/{lenv_append.ma => lenv_append.etc} | 0 .../lenv/{lenv_length.ma => lenv_length.etc} | 0 .../basic_2/grammar/term_vector.ma | 8 ++++++++ .../basic_2/notation/relations/rlift_4.ma | 19 ------------------- 4 files changed, 8 insertions(+), 19 deletions(-) rename matita/matita/contribs/lambdadelta/basic_2/etc_new/lenv/{lenv_append.ma => lenv_append.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/etc_new/lenv/{lenv_length.ma => lenv_length.etc} (100%) delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/notation/relations/rlift_4.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lenv/lenv_append.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lenv/lenv_append.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/lenv/lenv_append.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc_new/lenv/lenv_append.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lenv/lenv_length.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lenv/lenv_length.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/lenv/lenv_length.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc_new/lenv/lenv_length.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/term_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/term_vector.ma index 9575612e0..192b78637 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/term_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/term_vector.ma @@ -27,6 +27,14 @@ let rec applv Vs T on Vs ≝ interpretation "application to vector (term)" 'SnApplVector Vs T = (applv Vs T). +(* Basic properties *********************************************************) + +lemma applv_nil: ∀T. Ⓐ ◊.T = T. +// qed. + +lemma applv_cons: ∀V,Vs,T. Ⓐ V@Vs.T = ⓐV.ⒶVs.T. +// qed. + (* properties concerning simple terms ***************************************) lemma applv_simple: ∀T,Vs. 𝐒⦃T⦄ → 𝐒⦃ⒶVs.T⦄. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/rlift_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/rlift_4.ma deleted file mode 100644 index e2a03284e..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/rlift_4.ma +++ /dev/null @@ -1,19 +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 *) -(* *) -(**************************************************************************) - -(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) - -notation "hvbox( ⬆ [ term 46 l , break term 46 m ] break term 46 T1 ≡ break term 46 T2 )" - non associative with precedence 45 - for @{ 'RLift $l $m $T1 $T2 }. -- 2.39.2