From d6909ee6f43e0f29efbaf28b75b69723634c3af2 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 12 Sep 2014 18:26:30 +0000 Subject: [PATCH] bug fix in ththe notation for lists: disambiguation of nil does not work very well in gcp_cr and gcp_aaa :( --- .../lambdadelta/apps_2/functional/rtm.ma | 6 +++--- .../lambdadelta/apps_2/functional/rtm_step.ma | 4 ++-- .../basic_2/computation/gcp_aaa.ma | 14 +++++++------- .../lambdadelta/basic_2/computation/gcp_cr.ma | 15 +++++++-------- .../lambdadelta/basic_2/multiple/drops.ma | 6 +++--- .../lambdadelta/basic_2/multiple/lifts.ma | 6 +++--- .../lambdadelta/basic_2/multiple/mr2.ma | 6 +++--- .../lambdadelta/basic_2/multiple/mr2_minus.ma | 6 +++--- .../lambdadelta/basic_2/multiple/mr2_plus.ma | 4 ++-- .../lambdadelta/basic_2/web/basic_2_src.tbl | 2 +- .../contribs/lambdadelta/ground_2/lib/list.ma | 13 ++++++------- .../constructors/{nil_2.ma => cons_2.ma} | 6 +++--- .../ground_2/notation/constructors/cons_3.ma | 6 +++--- .../ground_2/notation/constructors/cons_5.ma | 19 ------------------- .../constructors/{nil_1.ma => nil_0.ma} | 2 +- 15 files changed, 47 insertions(+), 68 deletions(-) rename matita/matita/contribs/lambdadelta/ground_2/notation/constructors/{nil_2.ma => cons_2.ma} (91%) delete mode 100644 matita/matita/contribs/lambdadelta/ground_2/notation/constructors/cons_5.ma rename matita/matita/contribs/lambdadelta/ground_2/notation/constructors/{nil_1.ma => nil_0.ma} (98%) diff --git a/matita/matita/contribs/lambdadelta/apps_2/functional/rtm.ma b/matita/matita/contribs/lambdadelta/apps_2/functional/rtm.ma index 5153b713f..2e92ea0cc 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/functional/rtm.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/functional/rtm.ma @@ -44,18 +44,18 @@ record rtm: Type[0] ≝ (* initial state *) definition rtm_i: genv → term → rtm ≝ - λG,T. mk_rtm G 0 (⋆) (⟠) T. + λG,T. mk_rtm G 0 (⋆) (◊) T. (* update code *) definition rtm_t: rtm → term → rtm ≝ λM,T. match M with - [ mk_rtm G u E _ _ ⇒ mk_rtm G u E (⟠) T + [ mk_rtm G u E _ _ ⇒ mk_rtm G u E (◊) T ]. (* update closure *) definition rtm_u: rtm → xenv → term → rtm ≝ λM,E,T. match M with - [ mk_rtm G u _ _ _ ⇒ mk_rtm G u E (⟠) T + [ mk_rtm G u _ _ _ ⇒ mk_rtm G u E (◊) T ]. (* get global environment *) diff --git a/matita/matita/contribs/lambdadelta/apps_2/functional/rtm_step.ma b/matita/matita/contribs/lambdadelta/apps_2/functional/rtm_step.ma index ed77ca726..8f5a61ee8 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/functional/rtm_step.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/functional/rtm_step.ma @@ -46,8 +46,8 @@ inductive rtm_step: relation rtm ≝ rtm_step (mk_rtm G u E ({D, V} @ S) (+ⓛW. T)) (mk_rtm G u (E. ④{Abbr} {u, D, V}) S T) | rtm_push : ∀G,u,E,W,T. - rtm_step (mk_rtm G u E (⟠) (+ⓛW. T)) - (mk_rtm G (u + 1) (E. ④{Abst} {u, E, W}) (⟠) T) + rtm_step (mk_rtm G u E (◊) (+ⓛW. T)) + (mk_rtm G (u + 1) (E. ④{Abst} {u, E, W}) (◊) T) | rtm_theta : ∀G,u,E,S,V,T. rtm_step (mk_rtm G u E S (+ⓓV. T)) (mk_rtm G u (E. ④{Abbr} {u, E, V}) S T) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/gcp_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/gcp_aaa.ma index c890be39e..3522d41ac 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/gcp_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/gcp_aaa.ma @@ -32,7 +32,7 @@ theorem acr_aaa_csubc_lifts: ∀RR,RS,RP. [ #G #L #k #L0 #des #HL0 #X #H #L2 #HL20 >(lifts_inv_sort1 … H) -H lapply (acr_gcr … H1RP H2RP (⓪)) #HAtom - @(s4 … HAtom … (◊)) // + lapply (s4 … HAtom G L2 (◊)) /2 width=1 by/ | #I #G #L1 #K1 #V1 #B #i #HLK1 #HKV1B #IHB #L0 #des #HL01 #X #H #L2 #HL20 lapply (acr_gcr … H1RP H2RP B) #HB elim (lifts_inv_lref1 … H) -H #i1 #Hi1 #H destruct @@ -45,7 +45,7 @@ theorem acr_aaa_csubc_lifts: ∀RR,RS,RP. [ #K2 #HK20 #H destruct elim (lift_total V0 0 (i0 +1)) #V #HV0 elim (lifts_lift_trans … Hi0 … Hdes0 … HV10 … HV0) -HV10 #V2 #HV12 #HV2 - @(s5 … HB … (◊) … HV0 HLK2) /3 width=7 by drops_cons, lifts_cons/ (* Note: uses IHB HL20 V2 HV0 *) + lapply (s5 … HB ? G ? ? (◊) … HV0 HLK2) /3 width=7 by drops_cons, lifts_cons/ (* Note: uses IHB HL20 V2 HV0 *) | -HLK1 -IHB -HL01 -HL20 -HK1b -Hi0 -Hdes0 #K2 #V2 #A2 #HKV2A #H1KV0A #H2KV0A #_ #H1 #H2 destruct lapply (drop_fwd_drop2 … HLK2) #HLK2b @@ -53,22 +53,22 @@ theorem acr_aaa_csubc_lifts: ∀RR,RS,RP. lapply (aaa_mono … H2KV0A … HKV0B) #H destruct -H2KV0A -HKV0B elim (lift_total V0 0 (i0 +1)) #V3 #HV03 elim (lift_total V2 0 (i0 +1)) #V #HV2 - @(s5 … HB … (◊) … (ⓝV3.V) … HLK2) [2: /2 width=1 by lift_flat/ ] - @(s7 … HB … (◊)) [ @(s0 … HB … HKV2A) // | @(s0 … HB … H1KV0A) // ] + lapply (s5 … HB ? G ? ? (◊) … (ⓝV3.V) … HLK2) [1,3: /2 width=1 by lift_flat/ ] + lapply (s7 … HB G L2 (◊)) #H @H -H [ @(s0 … HB … HKV2A) // | @(s0 … HB … H1KV0A) // ] ] | #a #G #L #V #T #B #A #_ #_ #IHB #IHA #L0 #des #HL0 #X #H #L2 #HL20 elim (lifts_inv_bind1 … H) -H #V0 #T0 #HV0 #HT0 #H destruct lapply (acr_gcr … H1RP H2RP A) #HA lapply (acr_gcr … H1RP H2RP B) #HB lapply (s1 … HB) -HB #HB - @(s6 … HA … (◊) (◊)) /3 width=5 by lsubc_pair, drops_skip, liftv_nil/ + lapply (s6 … HA G L2 (◊) (◊)) /4 width=5 by lsubc_pair, drops_skip, liftv_nil/ | #a #G #L #W #T #B #A #HLWB #_ #IHB #IHA #L0 #des #HL0 #X #H #L2 #HL02 elim (lifts_inv_bind1 … H) -H #W0 #T0 #HW0 #HT0 #H destruct @(acr_abst … H1RP H2RP) [ /2 width=5 by/ ] #L3 #V3 #W3 #T3 #des3 #HL32 #HW03 #HT03 #H1B #H2B elim (drops_lsubc_trans … H1RP H2RP … HL32 … HL02) -L2 #L2 #HL32 #HL20 lapply (aaa_lifts … L2 W3 … (des @@ des3) … HLWB) -HLWB /2 width=4 by drops_trans, lifts_trans/ #HLW2B - @(IHA (L2. ⓛW3) … (des + 1 @@ des3 + 1)) -IHA + @(IHA (L2. ⓛW3) … (des + 1 @@ des3 + 1)) -IHA /3 width=5 by lsubc_beta, drops_trans, drops_skip, lifts_trans/ | #G #L #V #T #B #A #_ #_ #IHB #IHA #L0 #des #HL0 #X #H #L2 #HL20 elim (lifts_inv_flat1 … H) -H #V0 #T0 #HV0 #HT0 #H destruct @@ -76,7 +76,7 @@ theorem acr_aaa_csubc_lifts: ∀RR,RS,RP. | #G #L #V #T #A #_ #_ #IH1A #IH2A #L0 #des #HL0 #X #H #L2 #HL20 elim (lifts_inv_flat1 … H) -H #V0 #T0 #HV0 #HT0 #H destruct lapply (acr_gcr … H1RP H2RP A) #HA - @(s7 … HA … (◊)) /2 width=5 by/ + lapply (s7 … HA G L2 (◊)) /3 width=5 by/ ] qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/gcp_cr.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/gcp_cr.ma index 537769345..ca6b3df49 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/gcp_cr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/gcp_cr.ma @@ -116,14 +116,13 @@ qed. *) lemma acr_gcr: ∀RR,RS,RP. gcp RR RS RP → gcr RR RS RP RP → ∀A. gcr RR RS RP (acr RP A). -#RR #RS #RP #H1RP #H2RP #A elim A -A normalize // -#B #A #IHB #IHA @mk_gcr normalize +#RR #RS #RP #H1RP #H2RP #A elim A -A // +#B #A #IHB #IHA @mk_gcr [ /3 width=7 by drops_cons, lifts_cons/ | #G #L #T #H elim (cp1 … H1RP G L) #k #HK - lapply (H ? (⋆k) ? (⟠) ? ? ?) -H - [3,5: // |2,4: skip - | @(s2 … IHB … (◊)) // + lapply (H L (⋆k) T (◊) ? ? ?) -H // + [ lapply (s2 … IHB G L (◊) … HK) // | #H @(cp2 … H1RP … k) @(s1 … IHA) // ] | #G #L #Vs #HVs #T #H1T #H2T #L0 #V0 #X #des #HL0 #H #HB @@ -181,11 +180,11 @@ lapply (acr_gcr … H1RP H2RP A) #HCA lapply (acr_gcr … H1RP H2RP B) #HCB elim (lifts_inv_bind1 … H) -H #W0 #T0 #HW0 #HT0 #H destruct lapply (gcr_lifts … HL0 … HW0 HW) -HW [ @(s0 … HCB) ] #HW0 -@(s3 … HCA … (◊)) -@(s6 … HCA … (◊) (◊)) // +lapply (s3 … HCA … a G L0 (◊)) #H @H -H +lapply (s6 … HCA G L0 (◊) (◊) ?) // #H @H -H [ @(HA … HL0) // | lapply (s1 … HCB) -HCB #HCB - @(s7 … H2RP … (◊)) /2 width=1 by/ + lapply (s7 … H2RP G L0 (◊)) /3 width=1 by/ ] qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/drops.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/drops.ma index 1c0c18888..4508cf6a3 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/multiple/drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/drops.ma @@ -21,7 +21,7 @@ include "basic_2/multiple/lifts.ma". (* ITERATED LOCAL ENVIRONMENT SLICING ***************************************) inductive drops (s:bool): list2 nat nat → relation lenv ≝ -| drops_nil : ∀L. drops s (⟠) L L +| drops_nil : ∀L. drops s (◊) L L | drops_cons: ∀L1,L,L2,des,d,e. drops s des L1 L → ⇩[s, d, e] L ≡ L2 → drops s ({d, e} @ des) L1 L2 . @@ -35,13 +35,13 @@ interpretation "iterated slicing (local environment) general" (* Basic inversion lemmas ***************************************************) -fact drops_inv_nil_aux: ∀L1,L2,s,des. ⇩*[s, des] L1 ≡ L2 → des = ⟠ → L1 = L2. +fact drops_inv_nil_aux: ∀L1,L2,s,des. ⇩*[s, des] L1 ≡ L2 → des = ◊ → L1 = L2. #L1 #L2 #s #des * -L1 -L2 -des // #L1 #L #L2 #d #e #des #_ #_ #H destruct qed-. (* Basic_1: was: drop1_gen_pnil *) -lemma drops_inv_nil: ∀L1,L2,s. ⇩*[s, ⟠] L1 ≡ L2 → L1 = L2. +lemma drops_inv_nil: ∀L1,L2,s. ⇩*[s, ◊] L1 ≡ L2 → L1 = L2. /2 width=4 by drops_inv_nil_aux/ qed-. fact drops_inv_cons_aux: ∀L1,L2,s,des. ⇩*[s, des] L1 ≡ L2 → diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts.ma index 67e93078e..272105255 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts.ma @@ -19,7 +19,7 @@ include "basic_2/multiple/mr2_plus.ma". (* GENERIC TERM RELOCATION **************************************************) inductive lifts: list2 nat nat → relation term ≝ -| lifts_nil : ∀T. lifts (⟠) T T +| lifts_nil : ∀T. lifts (◊) T T | lifts_cons: ∀T1,T,T2,des,d,e. ⇧[d,e] T1 ≡ T → lifts des T T2 → lifts ({d, e} @ des) T1 T2 . @@ -29,12 +29,12 @@ interpretation "generic relocation (term)" (* Basic inversion lemmas ***************************************************) -fact lifts_inv_nil_aux: ∀T1,T2,des. ⇧*[des] T1 ≡ T2 → des = ⟠ → T1 = T2. +fact lifts_inv_nil_aux: ∀T1,T2,des. ⇧*[des] T1 ≡ T2 → des = ◊ → T1 = T2. #T1 #T2 #des * -T1 -T2 -des // #T1 #T #T2 #d #e #des #_ #_ #H destruct qed-. -lemma lifts_inv_nil: ∀T1,T2. ⇧*[⟠] T1 ≡ T2 → T1 = T2. +lemma lifts_inv_nil: ∀T1,T2. ⇧*[◊] T1 ≡ T2 → T1 = T2. /2 width=3 by lifts_inv_nil_aux/ qed-. fact lifts_inv_cons_aux: ∀T1,T2,des. ⇧*[des] T1 ≡ T2 → diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2.ma index bf4331b89..137c179fa 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2.ma @@ -18,7 +18,7 @@ include "basic_2/grammar/term_vector.ma". (* MULTIPLE RELOCATION WITH PAIRS *******************************************) inductive at: list2 nat nat → relation nat ≝ -| at_nil: ∀i. at (⟠) i i +| at_nil: ∀i. at (◊) i i | at_lt : ∀des,d,e,i1,i2. i1 < d → at des i1 i2 → at ({d, e} @ des) i1 i2 | at_ge : ∀des,d,e,i1,i2. d ≤ i1 → @@ -30,7 +30,7 @@ interpretation "application (multiple relocation with pairs)" (* Basic inversion lemmas ***************************************************) -fact at_inv_nil_aux: ∀des,i1,i2. @⦃i1, des⦄ ≡ i2 → des = ⟠ → i1 = i2. +fact at_inv_nil_aux: ∀des,i1,i2. @⦃i1, des⦄ ≡ i2 → des = ◊ → i1 = i2. #des #i1 #i2 * -des -i1 -i2 [ // | #des #d #e #i1 #i2 #_ #_ #H destruct @@ -38,7 +38,7 @@ fact at_inv_nil_aux: ∀des,i1,i2. @⦃i1, des⦄ ≡ i2 → des = ⟠ → i1 = ] qed-. -lemma at_inv_nil: ∀i1,i2. @⦃i1, ⟠⦄ ≡ i2 → i1 = i2. +lemma at_inv_nil: ∀i1,i2. @⦃i1, ◊⦄ ≡ i2 → i1 = i2. /2 width=3 by at_inv_nil_aux/ qed-. fact at_inv_cons_aux: ∀des,i1,i2. @⦃i1, des⦄ ≡ i2 → diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2_minus.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2_minus.ma index a60ba3956..a4f7bb851 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2_minus.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2_minus.ma @@ -18,7 +18,7 @@ include "basic_2/multiple/mr2.ma". (* MULTIPLE RELOCATION WITH PAIRS *******************************************) inductive minuss: nat → relation (list2 nat nat) ≝ -| minuss_nil: ∀i. minuss i (⟠) (⟠) +| minuss_nil: ∀i. minuss i (◊) (◊) | minuss_lt : ∀des1,des2,d,e,i. i < d → minuss i des1 des2 → minuss i ({d, e} @ des1) ({d - i, e} @ des2) | minuss_ge : ∀des1,des2,d,e,i. d ≤ i → minuss (e + i) des1 des2 → @@ -30,7 +30,7 @@ interpretation "minus (multiple relocation with pairs)" (* Basic inversion lemmas ***************************************************) -fact minuss_inv_nil1_aux: ∀des1,des2,i. des1 ▭ i ≡ des2 → des1 = ⟠ → des2 = ⟠. +fact minuss_inv_nil1_aux: ∀des1,des2,i. des1 ▭ i ≡ des2 → des1 = ◊ → des2 = ◊. #des1 #des2 #i * -des1 -des2 -i [ // | #des1 #des2 #d #e #i #_ #_ #H destruct @@ -38,7 +38,7 @@ fact minuss_inv_nil1_aux: ∀des1,des2,i. des1 ▭ i ≡ des2 → des1 = ⟠ → ] qed-. -lemma minuss_inv_nil1: ∀des2,i. ⟠ ▭ i ≡ des2 → des2 = ⟠. +lemma minuss_inv_nil1: ∀des2,i. ◊ ▭ i ≡ des2 → des2 = ◊. /2 width=4 by minuss_inv_nil1_aux/ qed-. fact minuss_inv_cons1_aux: ∀des1,des2,i. des1 ▭ i ≡ des2 → diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2_plus.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2_plus.ma index d589181ee..6528fb827 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2_plus.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2_plus.ma @@ -17,7 +17,7 @@ include "basic_2/multiple/mr2.ma". (* MULTIPLE RELOCATION WITH PAIRS *******************************************) let rec pluss (des:list2 nat nat) (i:nat) on des ≝ match des with -[ nil2 ⇒ ⟠ +[ nil2 ⇒ ◊ | cons2 d e des ⇒ {d + i, e} @ pluss des i ]. @@ -26,7 +26,7 @@ interpretation "plus (multiple relocation with pairs)" (* Basic inversion lemmas ***************************************************) -lemma pluss_inv_nil2: ∀i,des. des + i = ⟠ → des = ⟠. +lemma pluss_inv_nil2: ∀i,des. des + i = ◊ → des = ◊. #i * // normalize #d #e #des #H destruct qed. 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 b17fe1e42..3dd375cd3 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 @@ -12,7 +12,7 @@ table { class "wine" [ { "examples" * } { [ { "terms with special features" * } { - [ "ex_sta_ldec" "ex_cpr_omega" * ] + [ "ex_sta_ldec" + "ex_cpr_omega" * ] } ] } diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/list.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/list.ma index d21e1b52b..9355f9c56 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/lib/list.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/list.ma @@ -12,10 +12,9 @@ (* *) (**************************************************************************) -include "ground_2/notation/constructors/nil_1.ma". -include "ground_2/notation/constructors/nil_2.ma". +include "ground_2/notation/constructors/nil_0.ma". +include "ground_2/notation/constructors/cons_2.ma". include "ground_2/notation/constructors/cons_3.ma". -include "ground_2/notation/constructors/cons_5.ma". include "ground_2/notation/functions/append_2.ma". include "ground_2/lib/arith.ma". @@ -25,9 +24,9 @@ inductive list (A:Type[0]) : Type[0] := | nil : list A | cons: A → list A → list A. -interpretation "nil (list)" 'Nil A = (nil A). +interpretation "nil (list)" 'Nil = (nil ?). -interpretation "cons (list)" 'Cons A hd tl = (cons A hd tl). +interpretation "cons (list)" 'Cons hd tl = (cons ? hd tl). let rec all A (R:predicate A) (l:list A) on l ≝ match l with @@ -39,9 +38,9 @@ inductive list2 (A1,A2:Type[0]) : Type[0] := | nil2 : list2 A1 A2 | cons2: A1 → A2 → list2 A1 A2 → list2 A1 A2. -interpretation "nil (list of pairs)" 'Nil A1 A2 = (nil2 A1 A2). +interpretation "nil (list of pairs)" 'Nil = (nil2 ? ?). -interpretation "cons (list of pairs)" 'Cons A1 A2 hd1 hd2 tl = (cons2 A1 A2 hd1 hd2 tl). +interpretation "cons (list of pairs)" 'Cons hd1 hd2 tl = (cons2 ? ? hd1 hd2 tl). let rec append2 (A1,A2:Type[0]) (l1,l2:list2 A1 A2) on l1 ≝ match l1 with [ nil2 ⇒ l2 diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/nil_2.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/cons_2.ma similarity index 91% rename from matita/matita/contribs/lambdadelta/ground_2/notation/constructors/nil_2.ma rename to matita/matita/contribs/lambdadelta/ground_2/notation/constructors/cons_2.ma index 1a48e23f3..c95c57d8e 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/nil_2.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/cons_2.ma @@ -14,6 +14,6 @@ (* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) -notation "⟠" - non associative with precedence 46 - for @{ 'Nil ? ? }. +notation "hvbox( hd @ break tl )" + right associative with precedence 47 + for @{ 'Cons $hd $tl }. diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/cons_3.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/cons_3.ma index 97fd6e963..cfa556e68 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/cons_3.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/cons_3.ma @@ -14,6 +14,6 @@ (* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) -notation "hvbox( hd @ break tl )" - right associative with precedence 47 - for @{ 'Cons ? $hd $tl }. +notation "hvbox( { term 46 hd1 , break term 46 hd2 } @ break term 46 tl )" + non associative with precedence 47 + for @{ 'Cons $hd1 $hd2 $tl }. diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/cons_5.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/cons_5.ma deleted file mode 100644 index c8bf11f01..000000000 --- a/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/cons_5.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 *) -(* *) -(**************************************************************************) - -(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) - -notation "hvbox( { term 46 hd1 , break term 46 hd2 } @ break term 46 tl )" - non associative with precedence 47 - for @{ 'Cons ? ? $hd1 $hd2 $tl }. diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/nil_1.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/nil_0.ma similarity index 98% rename from matita/matita/contribs/lambdadelta/ground_2/notation/constructors/nil_1.ma rename to matita/matita/contribs/lambdadelta/ground_2/notation/constructors/nil_0.ma index a6c5e6d54..6ea5151a9 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/nil_1.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/nil_0.ma @@ -16,4 +16,4 @@ notation "◊" non associative with precedence 46 - for @{ 'Nil ? }. + for @{ 'Nil }. -- 2.39.2