From 8730061377260fd9d86f77b46635038e3c1411cc Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 27 Nov 2012 22:24:11 +0000 Subject: [PATCH] bug fix in notation precedences --- .../contribs/lambda/delifting_substitution.ma | 8 ++++---- matita/matita/contribs/lambda/lift.ma | 12 ++++++------ matita/matita/contribs/lambda/multiplicity.ma | 4 ++-- matita/matita/contribs/lambda/term.ma | 14 +++++++------- 4 files changed, 19 insertions(+), 19 deletions(-) diff --git a/matita/matita/contribs/lambda/delifting_substitution.ma b/matita/matita/contribs/lambda/delifting_substitution.ma index 6e648c9a8..344ad8490 100644 --- a/matita/matita/contribs/lambda/delifting_substitution.ma +++ b/matita/matita/contribs/lambda/delifting_substitution.ma @@ -27,12 +27,12 @@ interpretation "delifting substitution" 'DSubst C d M = (dsubst C d M). (* Note: the notation with "/" does not work *) -notation "hvbox( [ d ⬐ break C ] break term 55 M )" - non associative with precedence 55 +notation "hvbox( [ term 46 d ⬐ break term 46 C ] break term 46 M )" + non associative with precedence 46 for @{ 'DSubst $C $d $M }. -notation > "hvbox( [ ⬐ C ] break term 55 M )" - non associative with precedence 55 +notation > "hvbox( [ ⬐ term 46 C ] break term 46 M )" + non associative with precedence 46 for @{ 'DSubst $C 0 $M }. lemma dsubst_vref_lt: ∀i,d,C. i < d → [d ⬐ C] #i = #i. diff --git a/matita/matita/contribs/lambda/lift.ma b/matita/matita/contribs/lambda/lift.ma index f3e1df822..817c0c1d7 100644 --- a/matita/matita/contribs/lambda/lift.ma +++ b/matita/matita/contribs/lambda/lift.ma @@ -28,16 +28,16 @@ let rec lift h d M on M ≝ match M with interpretation "relocation" 'Lift h d M = (lift h d M). -notation "hvbox( ↑ [ d , break h ] break term 55 M )" - non associative with precedence 55 +notation "hvbox( ↑ [ term 46 d , break term 46 h ] break term 46 M )" + non associative with precedence 46 for @{ 'Lift $h $d $M }. -notation > "hvbox( ↑ [ h ] break term 55 M )" - non associative with precedence 55 +notation > "hvbox( ↑ [ term 46 h ] break term 46 M )" + non associative with precedence 46 for @{ 'Lift $h 0 $M }. -notation > "hvbox( ↑ term 55 M )" - non associative with precedence 55 +notation > "hvbox( ↑ term 46 M )" + non associative with precedence 46 for @{ 'Lift 1 0 $M }. lemma lift_vref_lt: ∀d,h,i. i < d → ↑[d, h] #i = #i. diff --git a/matita/matita/contribs/lambda/multiplicity.ma b/matita/matita/contribs/lambda/multiplicity.ma index d6d5af110..e8b72762b 100644 --- a/matita/matita/contribs/lambda/multiplicity.ma +++ b/matita/matita/contribs/lambda/multiplicity.ma @@ -26,8 +26,8 @@ let rec mult M on M ≝ match M with interpretation "multiplicity" 'Multiplicity M = (mult M). -notation "hvbox( #{M} )" - non associative with precedence 55 +notation "hvbox( #{ term 46 M } )" + non associative with precedence 90 for @{ 'Multiplicity $M }. lemma mult_positive: ∀M. 0 < #{M}. diff --git a/matita/matita/contribs/lambda/term.ma b/matita/matita/contribs/lambda/term.ma index a38508ada..2e6a6e0ec 100644 --- a/matita/matita/contribs/lambda/term.ma +++ b/matita/matita/contribs/lambda/term.ma @@ -37,17 +37,17 @@ interpretation "term construction (application)" 'Application C A = (Appl C A). notation "hvbox( # term 90 i )" - non associative with precedence 55 + non associative with precedence 90 for @{ 'VariableReferenceByIndex $i }. -notation "hvbox( 𝛌 . term 55 A )" - non associative with precedence 55 +notation "hvbox( 𝛌 . term 46 A )" + non associative with precedence 46 for @{ 'Abstraction $A }. -notation > "hvbox( 𝛌 term 55 A )" - non associative with precedence 55 +notation > "hvbox( 𝛌 term 46 A )" + non associative with precedence 46 for @{ 'Abstraction $A }. -notation "hvbox( @ term 55 C . break term 55 A )" - non associative with precedence 55 +notation "hvbox( @ term 46 C . break term 46 A )" + non associative with precedence 46 for @{ 'Application $C $A }. -- 2.39.2