- test.ma on the disambiguation bug moved to ONAG (just out of the way)

- lambdadelta: updated interpretation descriptions fix the disambiguation bug

diff --git a/matita/matita/contribs/ONAG/test.ma b/matita/matita/contribs/ONAG/test.ma
new file mode 100644 (file)
index 0000000..1f4fac5
--- /dev/null
+++ b/matita/matita/contribs/ONAG/test.ma
@@ -0,0 +1,39 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+universe constraint Type[0] < Type[1].
+
+notation "hvbox(a break \to b)"
+  right associative with precedence 20
+for @{ \forall $_:$a.$b }.
+
+notation "hvbox( * )"
+ non associative with precedence 90
+ for @{ 'B }.
+
+inductive l: Type[0] ≝ L: l.
+
+inductive g: Type[0] ≝ G: g.
+
+axiom f: l → Prop.
+
+interpretation "b" 'B = L.
+
+interpretation "b" 'B = G.
+
+(* FG: two interpretations of the same notation and with the same description
+       override eachother, so the description is not just informative
+*)
+
+axiom s: f *.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma
index 8c00d3a99d2911003f1f57a0f430e0e190221f1b..dde5b8ce56da459c505c7d95a54a2fa69998bae9 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma
@@ -14,7 +14,6 @@
 
 include "basic_2/notation/relations/ineint_5.ma".
 include "basic_2/grammar/aarity.ma".
-include "basic_2/grammar/genv.ma". (**) (* not needed, disambiguation error *)
 include "basic_2/substitution/gr2_gr2.ma". 
 include "basic_2/substitution/lifts_lift_vector.ma".
 include "basic_2/substitution/ldrops_ldrop.ma".

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma
index f25909b757436e51a8b667bfd6c4ec42d0c2d56a..73067163099e86ac55c972f9ce6063e78dea23ee 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "basic_2/reduction/lpx_ldrop.ma".
 include "basic_2/computation/cpxs_lift.ma".
-include "basic_2/reduction/lpx_ldrop.ma". (**) (* disambiguation error *)
 
 (* CONTEXT-SENSITIVE EXTENDED PARALLEL COMPUTATION ON TERMS *****************)
 

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lift.ma
index 5658ab3643f4a8bc5423f55c0962bf84a2f7b13d..6b52e5b00c0ab251b2f4a8325305b624eee8b333 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lift.ma
@@ -12,9 +12,9 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/computation/csn.ma". (**) (* disambiguation error *)
 include "basic_2/reduction/cnx_lift.ma".
 include "basic_2/computation/acp.ma".
+include "basic_2/computation/csn.ma".
 
 (* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************)
 

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lprs.ma
index b1cd89788529859486fac68ea7343398a548fed8..6e8431959463f9f3410b36dd3c01d78786c91c14 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/lprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lprs.ma
@@ -13,8 +13,8 @@
 (**************************************************************************)
 
 include "basic_2/notation/relations/predsnstar_3.ma".
-include "basic_2/reduction/lpr.ma". (**) (* disambiguation error *)
 include "basic_2/grammar/lpx_sn_tc.ma".
+include "basic_2/reduction/lpr.ma".
 
 (* SN PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ****************************)
 

diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/cl_weight.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/cl_weight.ma
index 063e7b05eb03f3c719b1b3499a6b53e2fecf4f5b..aa20d64db45300fba99e5c01762adbf50f8d8bce 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/grammar/cl_weight.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/cl_weight.ma
@@ -13,8 +13,8 @@
 (**************************************************************************)
 
 include "basic_2/notation/functions/weight_3.ma".
-include "basic_2/grammar/genv.ma". (**) (* including genv after lenv shows a disambiguation bug: only the last interpretation is considered *)
 include "basic_2/grammar/lenv_weight.ma".
+include "basic_2/grammar/genv.ma".
 
 (* WEIGHT OF A CLOSURE ******************************************************)
 

diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/genv.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/genv.ma
index 38757ca1643dad295ab0d5a814fbe1eb56e2929f..3308b79edf4a8d3bc4d1e8e307ba95c17531c5ef 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/grammar/genv.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/genv.ma
@@ -27,7 +27,7 @@ definition genv ≝ list2 bind2 term.
 interpretation "sort (global environment)"
    'Star = (nil2 bind2 term).
 
-interpretation "environment binding construction (binary)"
+interpretation "global environment binding construction (binary)"
    'DxBind2 L I T = (cons2 bind2 term I T L).
 
 interpretation "abbreviation (global environment)"

diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv.ma
index a15c5309b9b3308daae7f84e35b158d67e8a9296..909231ae809d6d26115076fce5818b00bb83da8d 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv.ma
@@ -29,7 +29,7 @@ inductive lenv: Type[0] ≝
 interpretation "sort (local environment)"
    'Star = LAtom.
 
-interpretation "environment binding construction (binary)"
+interpretation "local environment binding construction (binary)"
    'DxBind2 L I T = (LPair L I T).
 
 interpretation "abbreviation (local environment)"

diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/test.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/test.ma
deleted file mode 100644 (file)
index 1f4fac5..0000000
--- a/matita/matita/contribs/lambdadelta/basic_2/grammar/test.ma
+++ /dev/null
@@ -1,39 +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                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-universe constraint Type[0] < Type[1].
-
-notation "hvbox(a break \to b)"
-  right associative with precedence 20
-for @{ \forall $_:$a.$b }.
-
-notation "hvbox( * )"
- non associative with precedence 90
- for @{ 'B }.
-
-inductive l: Type[0] ≝ L: l.
-
-inductive g: Type[0] ≝ G: g.
-
-axiom f: l → Prop.
-
-interpretation "b" 'B = L.
-
-interpretation "b" 'B = G.
-
-(* FG: two interpretations of the same notation and with the same description
-       override eachother, so the description is not just informative
-*)
-
-axiom s: f *.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr.ma
index 970673d2ee55df9f081afc36ee9ea751df561870..8aab91761f8bad0dd52f533599e4619ca2b0bdc7 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr.ma
@@ -13,8 +13,8 @@
 (**************************************************************************)
 
 include "basic_2/notation/relations/predsn_3.ma".
+include "basic_2/grammar/lpx_sn.ma".
 include "basic_2/reduction/cpr.ma".
-include "basic_2/grammar/lpx_sn.ma". (**) (* disambiguation error *)
 
 (* SN PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS *****************************)
 

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma
index b3e872e407be30b2d6a979bcaa4809033ec2c5f9..f23cca2fc3166c644fd3da8ccfc3bec8f24f8255 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma
@@ -12,9 +12,9 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/reduction/lpr_ldrop.ma". (**) (* disambiguation error *)
 include "basic_2/grammar/lpx_sn_lpx_sn.ma".
 include "basic_2/substitution/fsupp.ma".
+include "basic_2/reduction/lpr_ldrop.ma".
 
 (* SN PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS *****************************)
 

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma
index d209bd4b0f094b93a5e2109e6a084306e458562c..6acb2858c46b174d964e00025c95b2201743f742 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma
@@ -20,7 +20,7 @@ include "basic_2/relocation/lift.ma".
 (* LOCAL ENVIRONMENT SLICING ************************************************)
 
 (* Basic_1: includes: drop_skip_bind *)
-inductive ldrop: nat → nat → relation lenv ≝
+inductive ldrop: relation4 nat nat lenv lenv ≝
 | ldrop_atom : ∀d. ldrop d 0 (⋆) (⋆)
 | ldrop_pair : ∀L,I,V. ldrop 0 0 (L. ⓑ{I} V) (L. ⓑ{I} V)
 | ldrop_ldrop: ∀L1,L2,I,V,e. ldrop 0 e L1 L2 → ldrop 0 (e + 1) (L1. ⓑ{I} V) L2

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lift.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lift.ma
index e48d22e20477b0b796a3f26d6a64d13df42bc563..ba117d867f12573db855baa9ca910921ae324bd8 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lift.ma
@@ -21,7 +21,7 @@ include "basic_2/grammar/term_simple.ma".
 (* Basic_1: includes:
             lift_sort lift_lref_lt lift_lref_ge lift_bind lift_flat
 *)
-inductive lift: nat → nat → relation term ≝
+inductive lift: relation4 nat nat term term ≝
 | lift_sort   : ∀k,d,e. lift d e (⋆k) (⋆k)
 | lift_lref_lt: ∀i,d,e. i < d → lift d e (#i) (#i)
 | lift_lref_ge: ∀i,d,e. d ≤ i → lift d e (#i) (#(i + e))

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsuba.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsuba.ma
index c6d4478deac85989ad44871cefd0a9b584eadec4..eab0ff0358cd9cf3e7e254500aab0b4a07af2dc8 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lsuba.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lsuba.ma
@@ -13,8 +13,8 @@
 (**************************************************************************)
 
 include "basic_2/notation/relations/lrsubeqa_3.ma".
-include "basic_2/static/aaa.ma". (**) (* disambiguation error *)
 include "basic_2/substitution/lsubr.ma".
+include "basic_2/static/aaa.ma".
 
 (* LOCAL ENVIRONMENT REFINEMENT FOR ATOMIC ARITY ASSIGNMENT *****************)
 

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/ssta.ma b/matita/matita/contribs/lambdadelta/basic_2/static/ssta.ma
index ac9033c53a1b19eeb14ccde8ae2c5cc2fd80754f..5bb8b879354cfb9e4c20275865f6d0a7c41a7ec7 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/static/ssta.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/ssta.ma
@@ -13,14 +13,14 @@
 (**************************************************************************)
 
 include "basic_2/notation/relations/statictype_7.ma".
-include "basic_2/grammar/genv.ma". (**) (* disambiguation error *)
+include "basic_2/grammar/genv.ma".
 include "basic_2/relocation/ldrop.ma".
 include "basic_2/static/sd.ma".
 
 (* STRATIFIED STATIC TYPE ASSIGNMENT ON TERMS *******************************)
 
 (* activate genv *)
-inductive ssta (h:sh) (g:sd h): nat → genv → lenv → relation term ≝
+inductive ssta (h:sh) (g:sd h): nat → relation4 genv lenv term term ≝
 | ssta_sort: ∀G,L,k,l. deg h g k l → ssta h g l G L (⋆k) (⋆(next h k))
 | ssta_ldef: ∀G,L,K,V,W,U,i,l. ⇩[0, i] L ≡ K. ⓓV → ssta h g l G K V W →
              ⇧[0, i + 1] W ≡ U → ssta h g l G L (#i) U
@@ -36,8 +36,8 @@ inductive ssta (h:sh) (g:sd h): nat → genv → lenv → relation term ≝
 interpretation "stratified static type assignment (term)"
    'StaticType h g G L T U l = (ssta h g l G L T U).
 
-definition ssta_step: ∀h. sd h → genv → lenv → relation term ≝ λh,g,G,L,T,U.
-                      ∃l. ⦃G, L⦄ ⊢ T •[h, g] ⦃l+1, U⦄.
+definition ssta_step: ∀h. sd h → relation4 genv lenv term term ≝
+                      λh,g,G,L,T,U. ∃l. ⦃G, L⦄ ⊢ T •[h, g] ⦃l+1, U⦄.
 
 (* Basic inversion lemmas ************************************************)
 

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/ssta_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/static/ssta_lift.ma
index e51c4e80582f17b2a639c8b0ebde9e53d68b2794..cf969115db06b1166f79e4dfbe69830e94f4ebe7 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/static/ssta_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/ssta_lift.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/static/ssta.ma". (**) (* disambiguation error *)
 include "basic_2/relocation/ldrop_ldrop.ma".
+include "basic_2/static/ssta.ma".
 
 (* STRATIFIED STATIC TYPE ASSIGNMENT ON TERMS *******************************)
 

diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/sstas.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/sstas.ma
index ce1aea36e711e7772515a49f2a31f2565680b4a8..de9ca8b0d1d3c22c158352c9f0821aab616cba29 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/sstas.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/sstas.ma
@@ -18,7 +18,7 @@ include "basic_2/static/ssta.ma".
 (* ITERATED STRATIFIED STATIC TYPE ASSIGNMENT FOR TERMS *********************)
 
 (* Note: includes: stass_refl *)
-definition sstas: ∀h. sd h → genv → lenv → relation term ≝
+definition sstas: ∀h. sd h → relation4 genv lenv term term ≝
                   λh,g,G,L. star … (ssta_step h g G L).
 
 interpretation "iterated stratified static type assignment (term)"

diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/unfold.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/unfold.ma
index c44939a334288e0e7aed252313ae8abe4829317a..160c6da76a5ad2ca417778a600f22f8e7e9fbaf0 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/unfold.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/unfold.ma
@@ -13,8 +13,8 @@
 (**************************************************************************)
 
 include "basic_2/notation/relations/unfold_4.ma".
-include "basic_2/grammar/genv.ma". (**) (* disambiguation error *)
 include "basic_2/grammar/lenv_append.ma".
+include "basic_2/grammar/genv.ma".
 include "basic_2/relocation/ldrop.ma".
 
 (* CONTEXT-SENSITIVE UNFOLD FOR TERMS ***************************************)