From: Ferruccio Guidi Date: Mon, 28 Oct 2013 19:37:36 +0000 (+0000) Subject: lazy equivalence for local environments is now defined X-Git-Tag: make_still_working~1058 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=56e23ea031f695e40879053ff09e97ecec2507e1;p=helm.git lazy equivalence for local environments is now defined its reflexivity reveals a bug in ldrop :( --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fleq.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fleq.ma index 2448b5260..da608196c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fleq.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/fleq_8.ma". +include "basic_2/notation/relations/lazyeq_8.ma". include "basic_2/computation/lpxs.ma". (* EQUIVALENT "BIG TREE" NORMAL FORMS ***************************************) @@ -24,7 +24,7 @@ definition fleq: ∀h. sd h → tri_relation genv lenv term ≝ interpretation "equivalent 'big tree' normal forms (closure)" - 'FLEq h g G1 L1 T1 G2 L2 T2 = (fleq h g G1 L1 T1 G2 L2 T2). + 'LazyEq h g G1 L1 T1 G2 L2 T2 = (fleq h g G1 L1 T1 G2 L2 T2). (* Basic_properties *********************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/fleq_8.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/fleq_8.ma deleted file mode 100644 index 4e30eb6fc..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/fleq_8.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 G1, break term 46 L1, break term 46 T1 ⦄ ⋕ break [ term 46 h , break term 46 g ] break ⦃ term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )" - non associative with precedence 45 - for @{ 'FLEq $h $g $G1 $L1 $T1 $G2 $L2 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_3.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_3.ma new file mode 100644 index 000000000..acae727a4 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_3.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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( L1 ⋕ break [ term 46 T ] break term 46 L2 )" + non associative with precedence 45 + for @{ 'LazyEq $T $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_6.ma new file mode 100644 index 000000000..105a47363 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_6.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 G1, break term 46 L1, break term 46 T1 ⦄ ⋕ break ⦃ term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )" + non associative with precedence 45 + for @{ 'LazyEq $G1 $L1 $T1 $G2 $L2 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_8.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_8.ma new file mode 100644 index 000000000..052b1ad75 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_8.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 G1, break term 46 L1, break term 46 T1 ⦄ ⋕ break [ term 46 h , break term 46 g ] break ⦃ term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )" + non associative with precedence 45 + for @{ 'LazyEq $h $g $G1 $L1 $T1 $G2 $L2 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl index d91e8d629..036726dcc 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl @@ -236,7 +236,11 @@ table { [ { "lazy equivalence for closures" * } { [ "fleq ( ⦃?,?,?⦄ ⋕ ⦃?,?,?⦄ )" "fleq_fleq" * ] } - ] + ] + [ { "lazy equivalence for local environments" * } { + [ "lleq ( ? ⋕[?] ? )" "lleq_fleq" * ] + } + ] [ { "global env. slicing" * } { [ "gdrop ( ⇩[?] ? ≡ ? )" "gdrop_gdrop" * ] }