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 2448b5260e643c94863d25b93d040cfd3e9b0b8e..da608196ccbd2b8e823bbbed1428038511564eb5 100644 (file)
--- 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 (file)
index 4e30eb6..0000000
--- 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 (file)
index 0000000..acae727
--- /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 (file)
index 0000000..105a473
--- /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 (file)
index 0000000..052b1ad
--- /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 d91e8d6293ade379ae0d362d785fef4c890f0efa..036726dcc59cc81d84709682de93e2114c20f869 100644 (file)
--- 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" * ]
           }