From eaaea3c18083de3e442e939768ff450d3b093911 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 26 Apr 2012 15:28:13 +0000 Subject: [PATCH] - notation (possibly affecting all .ma files): we shifted the precedence levels from 50 to 60 up by 5 and moved level 65 to 66. By so doing, we cleared level 50 for use in the specification of the formal system lambda_delta, where we use it for weakly binding constructors - lambda_delta: notation fixup (a couple of bugs were corrected) --- matita/matita/contribs/ICC/lamla.ma | 2 +- matita/matita/contribs/POPLmark/Fsub/adeq.ma | 2 +- matita/matita/contribs/POPLmark/Fsub/defn.ma | 8 +- .../matita/contribs/POPLmark/Fsub/defndb.ma | 8 +- .../contribs/dama/dama/models/q_bars.ma | 2 +- .../contribs/dama/dama_didactic/reals.ma | 2 +- .../dama_duality/classical_pointwise/sets.ma | 10 +- .../contribs/dama/dama_duality/excess.ma | 22 ++-- .../contribs/dama/dama_duality/infsup.ma | 26 ++-- .../contribs/dama/dama_duality/lattice.ma | 40 +++--- .../contribs/dama/dama_duality/limit.ma | 12 +- .../matita/contribs/dama/dama_duality/tend.ma | 2 +- .../bin/old/formal_topology.ma | 2 +- .../formal_topology/formal_topology.ma | 2 +- .../formal_topology/formal_topology2.ma | 2 +- matita/matita/contribs/igft/igft.ma | 6 +- .../apps_2/functional/notation.ma | 4 +- .../basic_2/computation/csn_lcpr.ma | 2 +- .../basic_2/computation/lsubc_ldrop.ma | 2 +- .../contribs/lambda_delta/basic_2/notation.ma | 120 +++++++++--------- .../lambda_delta/basic_2/unfold/ltpss.ma | 2 +- matita/matita/lib/arithmetics/bigops.ma | 2 +- matita/matita/lib/basics/core_notation.ma | 38 +++--- matita/matita/lib/basics/lists/list.ma | 2 +- .../lib/formal_topology/apply_functor.ma | 8 +- .../matita/lib/formal_topology/categories.ma | 12 +- .../matita/lib/formal_topology/o-algebra.ma | 14 +- .../lib/formal_topology/r-o-basic_pairs.ma | 2 +- matita/matita/lib/formal_topology/subsets.ma | 12 +- matita/matita/lib/lambda/lambda_notation.ma | 34 ++--- matita/matita/lib/lambdaN/lambda_notation.ma | 28 ++-- matita/matita/lib/re/lang.ma | 2 +- matita/matita/lib/re/moves.ma | 2 +- matita/matita/lib/re/re.ma | 10 +- matita/matita/lib/re/reb.ma | 24 ++-- .../matita/library/algebra/finite_groups.ma | 2 +- .../matita/library/dama/bishop_set_rewrite.ma | 18 +-- matita/matita/library/dama/russell_support.ma | 2 +- matita/matita/library/dama/uniform.ma | 2 +- matita/matita/library/datatypes/categories.ma | 4 +- .../matita/library/demo/power_derivative.ma | 4 +- .../library/didactic/exercises/duality.ma | 2 +- .../exercises/natural_deduction_theories.ma | 4 +- .../library/didactic/exercises/shannon.ma | 2 +- .../didactic/exercises/substitution.ma | 2 +- matita/matita/library/nat/pi_p.ma | 10 +- matita/matita/nlibrary/PTS/gpts.ma | 2 +- matita/matita/nlibrary/basics/list2.ma | 2 +- matita/matita/nlibrary/core_notation.ma | 38 +++--- matita/matita/nlibrary/logic/cprop.ma | 6 +- matita/matita/nlibrary/overlap/o-algebra.ma | 14 +- matita/matita/nlibrary/re/re-setoids.ma | 22 ++-- matita/matita/nlibrary/re/re.ma | 22 ++-- matita/matita/nlibrary/sets/categories2.ma | 2 +- matita/matita/nlibrary/sets/setoids.ma | 4 +- matita/matita/nlibrary/sets/setoids1.ma | 2 +- matita/matita/nlibrary/sets/setoids2.ma | 2 +- .../matita/nlibrary/topology/igft-setoid.ma | 10 +- matita/matita/nlibrary/topology/igft.ma | 12 +- .../re_complete/basics/core_notation.ma | 38 +++--- matita/matita/re_complete/basics/list.ma | 2 +- matita/matita/re_complete/lang.ma | 2 +- matita/matita/re_complete/moves.ma | 2 +- matita/matita/re_complete/re.ma | 10 +- matita/matita/tests/color.ma | 2 +- 65 files changed, 357 insertions(+), 357 deletions(-) diff --git a/matita/matita/contribs/ICC/lamla.ma b/matita/matita/contribs/ICC/lamla.ma index d54775375..4af4ff558 100644 --- a/matita/matita/contribs/ICC/lamla.ma +++ b/matita/matita/contribs/ICC/lamla.ma @@ -52,7 +52,7 @@ notation "𝟛" non associative with precedence 90 for @{ 'three }. interpretation "three" 'three = (Var (S (S (S O)))). notation "𝟜" non associative with precedence 90 for @{ 'four }. interpretation "four" 'four = (Var (S (S (S (S O))))). -notation < "a ­b" left associative with precedence 60 for @{ 'appl $a $b }. +notation < "a ­b" left associative with precedence 65 for @{ 'appl $a $b }. interpretation "appl" 'appl a b = (Appl a b). let rec lift (from:nat) (amount:nat) (what:PT) on what : PT ≝ diff --git a/matita/matita/contribs/POPLmark/Fsub/adeq.ma b/matita/matita/contribs/POPLmark/Fsub/adeq.ma index 2a0f730ab..bd1c40716 100644 --- a/matita/matita/contribs/POPLmark/Fsub/adeq.ma +++ b/matita/matita/contribs/POPLmark/Fsub/adeq.ma @@ -144,7 +144,7 @@ interpretation "Fsub names to LN env encoding" 'encode G = (encodeenv G). notation < "| T |" with precedence 25 for @{'abs $T}. interpretation "Fsub named type length" 'abs T = (nt_len T). interpretation "list length" 'abs l = (length ? l). -notation < "〈a,b〉 · T" with precedence 60 for @{'swap $a $b $T}. +notation < "〈a,b〉 · T" with precedence 65 for @{'swap $a $b $T}. interpretation "natural swap" 'swap a b n = (swap a b n). interpretation "Fsub name swap in a named type" 'swap a b T = (swap_NTyp a b T). interpretation "Fsub name swap in a LN type" 'swap a b T = (swap_Typ a b T). diff --git a/matita/matita/contribs/POPLmark/Fsub/defn.ma b/matita/matita/contribs/POPLmark/Fsub/defn.ma index 337fe2686..4e48e27de 100644 --- a/matita/matita/contribs/POPLmark/Fsub/defn.ma +++ b/matita/matita/contribs/POPLmark/Fsub/defn.ma @@ -108,9 +108,9 @@ notation "mstyle color #007f00 (hvbox(e ⊢ break t))" interpretation "Fsub WF type judgement" 'wftjudg e t = (WFType e t). notation > "\Forall S.T" - non associative with precedence 60 for @{ 'forall $S $T}. + non associative with precedence 65 for @{ 'forall $S $T}. notation < "hvbox(⊓ \sub S. break T)" - non associative with precedence 60 for @{ 'forall $S $T}. + non associative with precedence 65 for @{ 'forall $S $T}. interpretation "universal type" 'forall S T = (Forall S T). notation "#x" with precedence 79 for @{'tvar $x}. @@ -123,7 +123,7 @@ notation "⊤" with precedence 90 for @{'toptype}. interpretation "toptype" 'toptype = Top. notation "hvbox(s break ⇛ t)" - right associative with precedence 55 for @{ 'arrow $s $t }. + right associative with precedence 60 for @{ 'arrow $s $t }. interpretation "arrow type" 'arrow S T = (Arrow S T). notation "hvbox(S [#n ↦ T])" @@ -131,7 +131,7 @@ notation "hvbox(S [#n ↦ T])" interpretation "subst bound var" 'substvar S T n = (subst_type_nat S T n). notation "hvbox(!X ⊴ T)" - non associative with precedence 60 for @{ 'subtypebound $X $T }. + non associative with precedence 65 for @{ 'subtypebound $X $T }. interpretation "subtyping bound" 'subtypebound X T = (mk_bound true X T). (****** PROOFS ********) diff --git a/matita/matita/contribs/POPLmark/Fsub/defndb.ma b/matita/matita/contribs/POPLmark/Fsub/defndb.ma index 745090de4..69e0d400d 100644 --- a/matita/matita/contribs/POPLmark/Fsub/defndb.ma +++ b/matita/matita/contribs/POPLmark/Fsub/defndb.ma @@ -71,9 +71,9 @@ notation "hvbox(e ⊢ break ta ⊴ break tb)" interpretation "Fsub subtype judgement" 'subjudg e ta tb = (JSubtype e ta tb). notation > "hvbox(\Forall S.T)" - non associative with precedence 60 for @{ 'forall $S $T}. + non associative with precedence 65 for @{ 'forall $S $T}. notation < "hvbox('All' \sub S. break T)" - non associative with precedence 60 for @{ 'forall $S $T}. + non associative with precedence 65 for @{ 'forall $S $T}. interpretation "universal type" 'forall S T = (Forall S T). notation "#x" with precedence 79 for @{'tvar $x}. @@ -83,11 +83,11 @@ notation "⊤" with precedence 90 for @{'toptype}. interpretation "toptype" 'toptype = Top. notation "hvbox(s break ⇛ t)" - right associative with precedence 55 for @{ 'arrow $s $t }. + right associative with precedence 60 for @{ 'arrow $s $t }. interpretation "arrow type" 'arrow S T = (Arrow S T). notation "hvbox(⊴ T)" - non associative with precedence 60 for @{ 'subtypebound $T }. + non associative with precedence 65 for @{ 'subtypebound $T }. interpretation "subtyping bound" 'subtypebound T = (mk_bound true T). (****** PROOFS ********) diff --git a/matita/matita/contribs/dama/dama/models/q_bars.ma b/matita/matita/contribs/dama/dama/models/q_bars.ma index 2cad9ca2a..ef16cd2bc 100644 --- a/matita/matita/contribs/dama/dama/models/q_bars.ma +++ b/matita/matita/contribs/dama/dama/models/q_bars.ma @@ -196,6 +196,6 @@ cases (?:False); [ apply (q_lt_corefl ? H)| cases (q_lt_le_incompat ?? (q_neg_gt ?) (q_lt_to_le ?? H))] qed. -notation < "x \blacksquare" non associative with precedence 50 for @{'unpos $x}. +notation < "x \blacksquare" non associative with precedence 55 for @{'unpos $x}. interpretation "hide unpos proof" 'unpos x = (unpos x ?). diff --git a/matita/matita/contribs/dama/dama_didactic/reals.ma b/matita/matita/contribs/dama/dama_didactic/reals.ma index 4dffb53fb..1474d4b7d 100644 --- a/matita/matita/contribs/dama/dama_didactic/reals.ma +++ b/matita/matita/contribs/dama/dama_didactic/reals.ma @@ -32,7 +32,7 @@ interpretation "real plus" 'plus x y = (Rplus x y). interpretation "real opp" 'uminus x = (Ropp x). notation "hvbox(a break · b)" - right associative with precedence 55 + right associative with precedence 60 for @{ 'mult $a $b }. interpretation "real mult" 'mult x y = (Rmult x y). diff --git a/matita/matita/contribs/dama/dama_duality/classical_pointwise/sets.ma b/matita/matita/contribs/dama/dama_duality/classical_pointwise/sets.ma index 48f07c2d6..6033f4db2 100644 --- a/matita/matita/contribs/dama/dama_duality/classical_pointwise/sets.ma +++ b/matita/matita/contribs/dama/dama_duality/classical_pointwise/sets.ma @@ -22,12 +22,12 @@ definition set ≝ λX:Type.X → Prop. definition member_of : ∀X.set X → X → Prop≝ λX.λA:set X.λx.A x. -notation "hvbox(x break ∈ A)" with precedence 60 +notation "hvbox(x break ∈ A)" with precedence 65 for @{ 'member_of $x $A }. interpretation "Member of" 'member_of x A = (mk_member_of ? A x). -notation "hvbox(x break ∉ A)" with precedence 60 +notation "hvbox(x break ∉ A)" with precedence 65 for @{ 'not_member_of $x $A }. interpretation "Not member of" 'not_member_of x A = (Not (member_of ? A x)). @@ -40,7 +40,7 @@ interpretation "Emptyset" 'emptyset = (emptyset ?). definition subset: ∀X. set X → set X → Prop≝ λX.λA,B:set X.∀x. x ∈ A → x ∈ B. -notation "hvbox(A break ⊆ B)" with precedence 60 +notation "hvbox(A break ⊆ B)" with precedence 65 for @{ 'subset $A $B }. interpretation "Subset" 'subset A B = (subset ? A B). @@ -55,7 +55,7 @@ interpretation "Intersection" 'intersection A B = (intersection ? A B). definition union: ∀X. set X → set X → set X ≝ λX.λA,B:set X.λx. x ∈ A ∨ x ∈ B. -notation "hvbox(A break ∪ B)" with precedence 65 +notation "hvbox(A break ∪ B)" with precedence 66 for @{ 'union $A $B }. interpretation "Union" 'union A B = (union ? A B). @@ -72,7 +72,7 @@ interpretation "nth" 'nth A i = (nth ? A i). definition countable_union: ∀X. seq (set X) → set X ≝ λX.λA:seq (set X).λx.∃j.x ∈ A \sub j. -notation "∪ \sub (ident i opt (: ty)) B" with precedence 65 +notation "∪ \sub (ident i opt (: ty)) B" with precedence 66 for @{ 'big_union ${default @{(λ${ident i}:$ty.$B)} @{(λ${ident i}.$B)}}}. interpretation "countable_union" 'big_union η.t = (countable_union ? t). diff --git a/matita/matita/contribs/dama/dama_duality/excess.ma b/matita/matita/contribs/dama/dama_duality/excess.ma index d4f0db302..16cb8097e 100644 --- a/matita/matita/contribs/dama/dama_duality/excess.ma +++ b/matita/matita/contribs/dama/dama_duality/excess.ma @@ -61,7 +61,7 @@ record apartness : Type ≝ { ap_cotransitive: cotransitive ? ap_apart }. -notation "hvbox(a break # b)" non associative with precedence 50 for @{ 'apart $a $b}. +notation "hvbox(a break # b)" non associative with precedence 55 for @{ 'apart $a $b}. interpretation "apartness" 'apart x y = (ap_apart ? x y). definition apartness_of_excess_base: excess_base → apartness. @@ -125,7 +125,7 @@ qed. definition eq ≝ λA:apartness.λa,b:A. ¬ (a # b). -notation "hvbox(a break ≈ b)" non associative with precedence 50 for @{ 'napart $a $b}. +notation "hvbox(a break ≈ b)" non associative with precedence 55 for @{ 'napart $a $b}. interpretation "Apartness alikeness" 'napart a b = (eq ? a b). interpretation "Excess alikeness" 'napart a b = (eq (excess_base_OF_excess1 ?) a b). interpretation "Excess (dual) alikeness" 'napart a b = (eq (excess_base_OF_excess ?) a b). @@ -152,7 +152,7 @@ qed. lemma eq_trans:∀E:apartness.∀x,z,y:E.x ≈ y → y ≈ z → x ≈ z ≝ λE,x,y,z.eq_trans_ E x z y. -notation > "'Eq'≈" non associative with precedence 50 for @{'eqrewrite}. +notation > "'Eq'≈" non associative with precedence 55 for @{'eqrewrite}. interpretation "eq_rew" 'eqrewrite = (eq_trans ? ? ?). alias id "antisymmetric" = "cic:/matita/constructive_higher_order_relations/antisymmetric.con". @@ -196,9 +196,9 @@ intros (E z y x Exy Lxz); apply (le_transitive ???? Lxz); intro Xyz; apply Exy; apply exc2ap; left; assumption; qed. -notation > "'Le'≪" non associative with precedence 50 for @{'lerewritel}. +notation > "'Le'≪" non associative with precedence 55 for @{'lerewritel}. interpretation "le_rewl" 'lerewritel = (le_rewl ? ? ?). -notation > "'Le'≫" non associative with precedence 50 for @{'lerewriter}. +notation > "'Le'≫" non associative with precedence 55 for @{'lerewriter}. interpretation "le_rewr" 'lerewriter = (le_rewr ? ? ?). lemma ap_rewl: ∀A:apartness.∀x,z,y:A. x ≈ y → y # z → x # z. @@ -211,9 +211,9 @@ intros (A x z y Exy Azy); apply ap_symmetric; apply (ap_rewl ???? Exy); apply ap_symmetric; assumption; qed. -notation > "'Ap'≪" non associative with precedence 50 for @{'aprewritel}. +notation > "'Ap'≪" non associative with precedence 55 for @{'aprewritel}. interpretation "ap_rewl" 'aprewritel = (ap_rewl ? ? ?). -notation > "'Ap'≫" non associative with precedence 50 for @{'aprewriter}. +notation > "'Ap'≫" non associative with precedence 55 for @{'aprewriter}. interpretation "ap_rewr" 'aprewriter = (ap_rewr ? ? ?). alias symbol "napart" = "Apartness alikeness". @@ -227,9 +227,9 @@ intros (A x z y Exy Azy); elim (exc_cotransitive ???x Azy); [assumption] elim (Exy); apply exc2ap; left; assumption; qed. -notation > "'Ex'≪" non associative with precedence 50 for @{'excessrewritel}. +notation > "'Ex'≪" non associative with precedence 55 for @{'excessrewritel}. interpretation "exc_rewl" 'excessrewritel = (exc_rewl ? ? ?). -notation > "'Ex'≫" non associative with precedence 50 for @{'excessrewriter}. +notation > "'Ex'≫" non associative with precedence 55 for @{'excessrewriter}. interpretation "exc_rewr" 'excessrewriter = (exc_rewr ? ? ?). lemma lt_rewr: ∀A:excess.∀x,z,y:A. x ≈ y → z < y → z < x. @@ -242,9 +242,9 @@ intros (A x y z E H); split; elim H; [apply (Le≪ ? (eq_sym ??? E));| apply (Ap≪ ? E);] assumption; qed. -notation > "'Lt'≪" non associative with precedence 50 for @{'ltrewritel}. +notation > "'Lt'≪" non associative with precedence 55 for @{'ltrewritel}. interpretation "lt_rewl" 'ltrewritel = (lt_rewl ? ? ?). -notation > "'Lt'≫" non associative with precedence 50 for @{'ltrewriter}. +notation > "'Lt'≫" non associative with precedence 55 for @{'ltrewriter}. interpretation "lt_rewr" 'ltrewriter = (lt_rewr ? ? ?). lemma lt_le_transitive: ∀A:excess.∀x,y,z:A.x < y → y ≤ z → x < z. diff --git a/matita/matita/contribs/dama/dama_duality/infsup.ma b/matita/matita/contribs/dama/dama_duality/infsup.ma index b5ff03f0a..f03a644dc 100644 --- a/matita/matita/contribs/dama/dama_duality/infsup.ma +++ b/matita/matita/contribs/dama/dama_duality/infsup.ma @@ -25,19 +25,19 @@ definition strong_sup ≝ definition increasing ≝ λO:excess.λa:sequence O.∀n:nat.a n ≤ a (S n). -notation < "x \nbsp 'is_upper_bound' \nbsp s" non associative with precedence 50 for @{'upper_bound $_ $s $x}. -notation < "x \nbsp 'is_lower_bound' \nbsp s" non associative with precedence 50 for @{'lower_bound $_ $s $x}. -notation < "s \nbsp 'is_increasing'" non associative with precedence 50 for @{'increasing $_ $s}. -notation < "s \nbsp 'is_decreasing'" non associative with precedence 50 for @{'decreasing $_ $s}. -notation < "x \nbsp 'is_strong_sup' \nbsp s" non associative with precedence 50 for @{'strong_sup $_ $s $x}. -notation < "x \nbsp 'is_strong_inf' \nbsp s" non associative with precedence 50 for @{'strong_inf $_ $s $x}. - -notation > "x 'is_upper_bound' s 'in' e" non associative with precedence 50 for @{'upper_bound $e $s $x}. -notation > "x 'is_lower_bound' s 'in' e" non associative with precedence 50 for @{'lower_bound $e $s $x}. -notation > "s 'is_increasing' 'in' e" non associative with precedence 50 for @{'increasing $e $s}. -notation > "s 'is_decreasing' 'in' e" non associative with precedence 50 for @{'decreasing $e $s}. -notation > "x 'is_strong_sup' s 'in' e" non associative with precedence 50 for @{'strong_sup $e $s $x}. -notation > "x 'is_strong_inf' s 'in' e" non associative with precedence 50 for @{'strong_inf $e $s $x}. +notation < "x \nbsp 'is_upper_bound' \nbsp s" non associative with precedence 55 for @{'upper_bound $_ $s $x}. +notation < "x \nbsp 'is_lower_bound' \nbsp s" non associative with precedence 55 for @{'lower_bound $_ $s $x}. +notation < "s \nbsp 'is_increasing'" non associative with precedence 55 for @{'increasing $_ $s}. +notation < "s \nbsp 'is_decreasing'" non associative with precedence 55 for @{'decreasing $_ $s}. +notation < "x \nbsp 'is_strong_sup' \nbsp s" non associative with precedence 55 for @{'strong_sup $_ $s $x}. +notation < "x \nbsp 'is_strong_inf' \nbsp s" non associative with precedence 55 for @{'strong_inf $_ $s $x}. + +notation > "x 'is_upper_bound' s 'in' e" non associative with precedence 55 for @{'upper_bound $e $s $x}. +notation > "x 'is_lower_bound' s 'in' e" non associative with precedence 55 for @{'lower_bound $e $s $x}. +notation > "s 'is_increasing' 'in' e" non associative with precedence 55 for @{'increasing $e $s}. +notation > "s 'is_decreasing' 'in' e" non associative with precedence 55 for @{'decreasing $e $s}. +notation > "x 'is_strong_sup' s 'in' e" non associative with precedence 55 for @{'strong_sup $e $s $x}. +notation > "x 'is_strong_inf' s 'in' e" non associative with precedence 55 for @{'strong_inf $e $s $x}. interpretation "Excess upper bound" 'upper_bound e s x = (upper_bound e s x). interpretation "Excess lower bound" 'lower_bound e s x = (upper_bound (dual_exc e) s x). diff --git a/matita/matita/contribs/dama/dama_duality/lattice.ma b/matita/matita/contribs/dama/dama_duality/lattice.ma index 877563afb..ae33bf9ec 100644 --- a/matita/matita/contribs/dama/dama_duality/lattice.ma +++ b/matita/matita/contribs/dama/dama_duality/lattice.ma @@ -23,7 +23,7 @@ record semi_lattice_base : Type ≝ { sl_strong_extop: ∀x.strong_ext ? (sl_op x) }. -notation "a \cross b" left associative with precedence 50 for @{ 'op $a $b }. +notation "a \cross b" left associative with precedence 55 for @{ 'op $a $b }. interpretation "semi lattice base operation" 'op a b = (sl_op ? a b). lemma excess_of_semi_lattice_base: semi_lattice_base → excess. @@ -182,7 +182,7 @@ qed. definition hole ≝ λT:Type.λx:T.x. -notation < "\ldots" non associative with precedence 50 for @{'hole}. +notation < "\ldots" non associative with precedence 55 for @{'hole}. interpretation "hole" 'hole = (hole ? ?). (* SL(E,M,H2-5(#),H67(≰)) → E' → c E = c E' → H67'(≰') → SL(E,M,p2-5,H67') *) @@ -423,20 +423,20 @@ record lattice : Type ≝ { absorbmj: ∀f,g:latt_carr. (f ∧ (f ∨ g)) ≈ f }. -notation "'meet'" non associative with precedence 50 for @{'meet}. -notation "'meet_refl'" non associative with precedence 50 for @{'meet_refl}. -notation "'meet_comm'" non associative with precedence 50 for @{'meet_comm}. -notation "'meet_assoc'" non associative with precedence 50 for @{'meet_assoc}. -notation "'strong_extm'" non associative with precedence 50 for @{'strong_extm}. -notation "'le_to_eqm'" non associative with precedence 50 for @{'le_to_eqm}. -notation "'lem'" non associative with precedence 50 for @{'lem}. -notation "'join'" non associative with precedence 50 for @{'join}. -notation "'join_refl'" non associative with precedence 50 for @{'join_refl}. -notation "'join_comm'" non associative with precedence 50 for @{'join_comm}. -notation "'join_assoc'" non associative with precedence 50 for @{'join_assoc}. -notation "'strong_extj'" non associative with precedence 50 for @{'strong_extj}. -notation "'le_to_eqj'" non associative with precedence 50 for @{'le_to_eqj}. -notation "'lej'" non associative with precedence 50 for @{'lej}. +notation "'meet'" non associative with precedence 55 for @{'meet}. +notation "'meet_refl'" non associative with precedence 55 for @{'meet_refl}. +notation "'meet_comm'" non associative with precedence 55 for @{'meet_comm}. +notation "'meet_assoc'" non associative with precedence 55 for @{'meet_assoc}. +notation "'strong_extm'" non associative with precedence 55 for @{'strong_extm}. +notation "'le_to_eqm'" non associative with precedence 55 for @{'le_to_eqm}. +notation "'lem'" non associative with precedence 55 for @{'lem}. +notation "'join'" non associative with precedence 55 for @{'join}. +notation "'join_refl'" non associative with precedence 55 for @{'join_refl}. +notation "'join_comm'" non associative with precedence 55 for @{'join_comm}. +notation "'join_assoc'" non associative with precedence 55 for @{'join_assoc}. +notation "'strong_extj'" non associative with precedence 55 for @{'strong_extj}. +notation "'le_to_eqj'" non associative with precedence 55 for @{'le_to_eqj}. +notation "'lej'" non associative with precedence 55 for @{'lej}. interpretation "Lattice meet" 'meet = (sl_meet (latt_mcarr ?)). interpretation "Lattice meet_refl" 'meet_refl = (sl_meet_refl (latt_mcarr ?)). @@ -453,10 +453,10 @@ interpretation "Lattice strong_extm" 'strong_extj = (sl_strong_extm (latt_jcarr interpretation "Lattice le_to_eqj" 'le_to_eqj = (sl_le_to_eqm (latt_jcarr ?)). interpretation "Lattice lej" 'lej = (sl_lem (latt_jcarr ?)). -notation "'feq_jl'" non associative with precedence 50 for @{'feq_jl}. -notation "'feq_jr'" non associative with precedence 50 for @{'feq_jr}. -notation "'feq_ml'" non associative with precedence 50 for @{'feq_ml}. -notation "'feq_mr'" non associative with precedence 50 for @{'feq_mr}. +notation "'feq_jl'" non associative with precedence 55 for @{'feq_jl}. +notation "'feq_jr'" non associative with precedence 55 for @{'feq_jr}. +notation "'feq_ml'" non associative with precedence 55 for @{'feq_ml}. +notation "'feq_mr'" non associative with precedence 55 for @{'feq_mr}. interpretation "Lattice feq_jl" 'feq_jl = (sl_feq_ml (latt_jcarr ?)). interpretation "Lattice feq_jr" 'feq_jr = (sl_feq_mr (latt_jcarr ?)). interpretation "Lattice feq_ml" 'feq_ml = (sl_feq_ml (latt_mcarr ?)). diff --git a/matita/matita/contribs/dama/dama_duality/limit.ma b/matita/matita/contribs/dama/dama_duality/limit.ma index 0b1bd1d3b..5d97d0ae6 100644 --- a/matita/matita/contribs/dama/dama_duality/limit.ma +++ b/matita/matita/contribs/dama/dama_duality/limit.ma @@ -22,10 +22,10 @@ definition limsup ≝ (∀k.(alpha k) is_strong_sup (shift ? xn k) in E) ∧ x is_strong_inf alpha in E. -notation < "x \nbsp 'is_limsup' \nbsp s" non associative with precedence 50 for @{'limsup $_ $s $x}. -notation < "x \nbsp 'is_liminf' \nbsp s" non associative with precedence 50 for @{'liminf $_ $s $x}. -notation > "x 'is_limsup' s 'in' e" non associative with precedence 50 for @{'limsup $e $s $x}. -notation > "x 'is_liminf' s 'in' e" non associative with precedence 50 for @{'liminf $e $s $x}. +notation < "x \nbsp 'is_limsup' \nbsp s" non associative with precedence 55 for @{'limsup $_ $s $x}. +notation < "x \nbsp 'is_liminf' \nbsp s" non associative with precedence 55 for @{'liminf $_ $s $x}. +notation > "x 'is_limsup' s 'in' e" non associative with precedence 55 for @{'limsup $e $s $x}. +notation > "x 'is_liminf' s 'in' e" non associative with precedence 55 for @{'liminf $e $s $x}. interpretation "Excess limsup" 'limsup e s x = (limsup e s x). interpretation "Excess liminf" 'liminf e s x = (limsup (dual_exc e) s x). @@ -34,8 +34,8 @@ interpretation "Excess liminf" 'liminf e s x = (limsup (dual_exc e) s x). definition lim ≝ λE:excess.λxn:sequence E.λx:E. x is_limsup xn in E ∧ x is_liminf xn in E. -notation < "x \nbsp 'is_lim' \nbsp s" non associative with precedence 50 for @{'lim $_ $s $x}. -notation > "x 'is_lim' s 'in' e" non associative with precedence 50 for @{'lim $e $s $x}. +notation < "x \nbsp 'is_lim' \nbsp s" non associative with precedence 55 for @{'lim $_ $s $x}. +notation > "x 'is_lim' s 'in' e" non associative with precedence 55 for @{'lim $e $s $x}. interpretation "Excess lim" 'lim e s x = (lim e s x). lemma sup_decreasing: diff --git a/matita/matita/contribs/dama/dama_duality/tend.ma b/matita/matita/contribs/dama/dama_duality/tend.ma index a9372d26d..1d14b49ab 100644 --- a/matita/matita/contribs/dama/dama_duality/tend.ma +++ b/matita/matita/contribs/dama/dama_duality/tend.ma @@ -22,6 +22,6 @@ definition tends0 ≝ definition d2s ≝ λR.λms:metric_space R.λs:sequence ms.λk.λn. δ (s n) k. -notation "s ⇝ x" non associative with precedence 50 for @{'tends $s $x}. +notation "s ⇝ x" non associative with precedence 55 for @{'tends $s $x}. interpretation "tends to" 'tends s x = (tends0 ? (d2s ? ? s x)). diff --git a/matita/matita/contribs/formal_topology/bin/old/formal_topology.ma b/matita/matita/contribs/formal_topology/bin/old/formal_topology.ma index e84c0242e..6c4ff9d0c 100644 --- a/matita/matita/contribs/formal_topology/bin/old/formal_topology.ma +++ b/matita/matita/contribs/formal_topology/bin/old/formal_topology.ma @@ -19,7 +19,7 @@ axiom S: Type. axiom leq: S → S → Prop. -notation "hvbox(A break ⊆ B)" with precedence 59 +notation "hvbox(A break ⊆ B)" with precedence 64 for @{ 'subseteq $A $B}. interpretation "Subseteq" 'subseteq A B = (leq A B). diff --git a/matita/matita/contribs/formal_topology/formal_topology.ma b/matita/matita/contribs/formal_topology/formal_topology.ma index 34a521f35..b22bc7fe3 100644 --- a/matita/matita/contribs/formal_topology/formal_topology.ma +++ b/matita/matita/contribs/formal_topology/formal_topology.ma @@ -19,7 +19,7 @@ axiom S: Type. axiom leq: S → S → Prop. -notation "hvbox(A break ⊆ B)" with precedence 59 +notation "hvbox(A break ⊆ B)" with precedence 64 for @{ 'subseteq $A $B}. interpretation "Subseteq" 'subseteq A B = (leq A B). diff --git a/matita/matita/contribs/formal_topology/formal_topology2.ma b/matita/matita/contribs/formal_topology/formal_topology2.ma index 0896edc5c..d236efed8 100644 --- a/matita/matita/contribs/formal_topology/formal_topology2.ma +++ b/matita/matita/contribs/formal_topology/formal_topology2.ma @@ -35,7 +35,7 @@ axiom one_right: ∀A:S. A 1 = A. axiom eps: S. axiom eps_idempotent: eps = eps eps. -notation "hvbox(A break ⊆ B)" with precedence 59 +notation "hvbox(A break ⊆ B)" with precedence 64 for @{ 'subseteq $A $B}. interpretation "Subseteq" 'subseteq A B = (eq ? A (comp eps B)). diff --git a/matita/matita/contribs/igft/igft.ma b/matita/matita/contribs/igft/igft.ma index 5fda91454..902ad692f 100644 --- a/matita/matita/contribs/igft/igft.ma +++ b/matita/matita/contribs/igft/igft.ma @@ -1,8 +1,8 @@ record powerset (A : Type) : Type := { content : A → CProp }. -notation > "Ω ^ A" non associative with precedence 50 for @{'P $A}. -notation "Ω \sup A" non associative with precedence 50 for @{'P $A}. +notation > "Ω ^ A" non associative with precedence 55 for @{'P $A}. +notation "Ω \sup A" non associative with precedence 55 for @{'P $A}. interpretation "Powerset" 'P A = (powerset A). record AxiomSet : Type := { @@ -30,7 +30,7 @@ interpretation "C a i" 'C2 a i = (C_ ? a i). definition in_subset := λA:AxiomSet.λa∈A.λU:Ω^A.content A U a. -notation "hvbox(a break εU)" non associative with precedence 50 for +notation "hvbox(a break εU)" non associative with precedence 55 for @{'in_subset $a $U}. interpretation "In subset" 'in_subset a U = (in_subset ? a U). diff --git a/matita/matita/contribs/lambda_delta/apps_2/functional/notation.ma b/matita/matita/contribs/lambda_delta/apps_2/functional/notation.ma index 48df845c1..031b745e4 100644 --- a/matita/matita/contribs/lambda_delta/apps_2/functional/notation.ma +++ b/matita/matita/contribs/lambda_delta/apps_2/functional/notation.ma @@ -15,11 +15,11 @@ (* NOTATION FOR THE "functional" COMPONENT ********************************) notation "hvbox( ↑ [ d , break e ] break T )" - non associative with precedence 55 + non associative with precedence 60 for @{ 'Lift $d $e $T }. notation "hvbox( [ d ← break V ] break T )" - non associative with precedence 55 + non associative with precedence 60 for @{ 'Subst $V $d $T }. notation "hvbox( T1 ⇨ break T2 )" diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lcpr.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lcpr.ma index c6024fce8..92d30c7fd 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lcpr.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lcpr.ma @@ -70,7 +70,7 @@ elim (cpr_inv_appl1 … H) -H * qed. (* Basic_1: was: sn3_beta *) -lemma csn_appl_beta: ∀L,W. L ⊢ ⬇* W → ∀V,T. L ⊢ ⬇* (ⓓV. T) → (**) +lemma csn_appl_beta: ∀L,W. L ⊢ ⬇* W → ∀V,T. L ⊢ ⬇* ⓓV. T → L ⊢ ⬇* ⓐV. ⓛW. T. /2 width=3/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/lsubc_ldrop.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/lsubc_ldrop.ma index 838986a8f..7d23f9e03 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/lsubc_ldrop.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/lsubc_ldrop.ma @@ -21,7 +21,7 @@ include "basic_2/computation/lsubc.ma". (* Properties concerning basic local environment slicing ********************) (* Basic_1: was: csubc_drop_conf_O *) -(* Note: the constant (0) can not be generalized *) +(* Note: the constant 0 can not be generalized *) lemma lsubc_ldrop_O1_trans: ∀RP,L1,L2. L1 [RP] ⊑ L2 → ∀K2,e. ⇩[0, e] L2 ≡ K2 → ∃∃K1. ⇩[0, e] L1 ≡ K1 & K1 [RP] ⊑ K2. #RP #L1 #L2 #H elim H -L1 -L2 diff --git a/matita/matita/contribs/lambda_delta/basic_2/notation.ma b/matita/matita/contribs/lambda_delta/basic_2/notation.ma index 9d0c9e34b..ae40690e7 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/notation.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/notation.ma @@ -40,48 +40,48 @@ notation "hvbox( § term 90 p )" non associative with precedence 90 for @{ 'GRef $p }. -notation "hvbox( ② term 90 T1 . break term 90 T )" - non associative with precedence 90 +notation "hvbox( ② term 55 T1 . break term 55 T )" + non associative with precedence 55 for @{ 'SnItem2 $T1 $T }. -notation "hvbox( ② { I } break term 90 T1 . break term 90 T )" - non associative with precedence 90 +notation "hvbox( ② { I } break term 55 T1 . break term 55 T )" + non associative with precedence 55 for @{ 'SnItem2 $I $T1 $T }. -notation "hvbox( ⓑ { I } break term 90 T1 . break term 90 T )" - non associative with precedence 90 +notation "hvbox( ⓑ { I } break term 55 T1 . break term 55 T )" + non associative with precedence 55 for @{ 'SnBind2 $I $T1 $T }. -notation "hvbox( ⓕ { I } break term 90 T1 . break term 90 T )" - non associative with precedence 90 +notation "hvbox( ⓕ { I } break term 55 T1 . break term 55 T )" + non associative with precedence 55 for @{ 'SnFlat2 $I $T1 $T }. -notation "hvbox( ⓓ term 90 T1 . break term 90 T2 )" - non associative with precedence 90 +notation "hvbox( ⓓ term 55 T1 . break term 55 T2 )" + non associative with precedence 55 for @{ 'SnAbbr $T1 $T2 }. -notation "hvbox( ⓛ term 90 T1 . break term 90 T2 )" - non associative with precedence 90 +notation "hvbox( ⓛ term 55 T1 . break term 55 T2 )" + non associative with precedence 55 for @{ 'SnAbst $T1 $T2 }. -notation "hvbox( ⓐ term 90 T1 . break term 90 T2 )" - non associative with precedence 90 +notation "hvbox( ⓐ term 55 T1 . break term 55 T2 )" + non associative with precedence 55 for @{ 'SnAppl $T1 $T2 }. -notation "hvbox( ⓣ term 90 T1 . break term 90 T2 )" - non associative with precedence 90 +notation "hvbox( ⓣ term 55 T1 . break term 55 T2 )" + non associative with precedence 55 for @{ 'SnCast $T1 $T2 }. -notation "hvbox( Ⓐ term 90 T1 . break term 90 T )" - non associative with precedence 90 +notation "hvbox( Ⓐ term 55 T1 . break term 55 T )" + non associative with precedence 55 for @{ 'SnApplV $T1 $T }. notation > "hvbox( T . break ②{ I } break term 47 T1 )" non associative with precedence 46 for @{ 'DxBind2 $T $I $T1 }. -notation "hvbox( T . break ⓑ { I } break term 90 T1 )" - non associative with precedence 89 +notation "hvbox( T . break ⓑ { I } break term 48 T1 )" + non associative with precedence 47 for @{ 'DxBind2 $T $I $T1 }. notation "hvbox( T1 . break ⓓ T2 )" @@ -93,7 +93,7 @@ notation "hvbox( T1 . break ⓛ T2 )" for @{ 'DxAbst $T1 $T2 }. notation "hvbox( T . break ④ { I } break { T1 , break T2 , break T3 } )" - non associative with precedence 47 + non associative with precedence 50 for @{ 'DxItem4 $T $I $T1 $T2 $T3 }. notation "hvbox( # [ x ] )" @@ -108,15 +108,15 @@ notation "hvbox( 𝐒 [ T ] )" non associative with precedence 45 for @{ 'Simple $T }. -notation "hvbox( L ⊢ break term 90 T1 ≈ break T2 )" +notation "hvbox( L ⊢ break term 46 T1 ≈ break term 46 T2 )" non associative with precedence 45 for @{ 'Hom $L $T1 $T2 }. -notation "hvbox( T1 ≃ break T2 )" +notation "hvbox( T1 ≃ break term 46 T2 )" non associative with precedence 45 for @{ 'Iso $T1 $T2 }. -notation "hvbox( T1 break [ d , break e ] ≼ break T2 )" +notation "hvbox( T1 break [ d , break e ] ≼ break term 46 T2 )" non associative with precedence 45 for @{ 'SubEq $T1 $d $e $T2 }. @@ -134,61 +134,61 @@ notation "hvbox( L ⊢ break [ d , break e ] break 𝐍 [ T ] )" non associative with precedence 45 for @{ 'Normal $L $d $e $T }. -notation "hvbox( ⇧ [ d , break e ] break T1 ≡ break T2 )" +notation "hvbox( ⇧ [ d , break e ] break term 46 T1 ≡ break term 46 T2 )" non associative with precedence 45 for @{ 'RLift $d $e $T1 $T2 }. -notation "hvbox( ⇩ [ e ] break L1 ≡ break L2 )" +notation "hvbox( ⇩ [ e ] break term 46 L1 ≡ break term 46 L2 )" non associative with precedence 45 for @{ 'RDrop $e $L1 $L2 }. -notation "hvbox( ⇩ [ d , break e ] break L1 ≡ break L2 )" +notation "hvbox( ⇩ [ d , break e ] break term 46 L1 ≡ break term 46 L2 )" non associative with precedence 45 for @{ 'RDrop $d $e $L1 $L2 }. -notation "hvbox( L ⊢ break ⌘ [ T ] ≡ break k )" +notation "hvbox( L ⊢ break ⌘ [ T ] ≡ break term 46 k )" non associative with precedence 45 for @{ 'ICM $L $T $k }. -notation "hvbox( L ⊢ break term 90 T1 break [ d , break e ] ▶ break T2 )" +notation "hvbox( L ⊢ break term 46 T1 break [ d , break e ] ▶ break term 46 T2 )" non associative with precedence 45 for @{ 'PSubst $L $T1 $d $e $T2 }. (* Unfold *******************************************************************) -notation "hvbox( @ [ T1 ] break f ≡ break T2 )" +notation "hvbox( @ [ T1 ] break term 46 f ≡ break term 46 T2 )" non associative with precedence 45 for @{ 'RAt $T1 $f $T2 }. -notation "hvbox( T1 ▭ break T2 ≡ break T )" +notation "hvbox( T1 ▭ break term 46 T2 ≡ break term 46 T )" non associative with precedence 45 for @{ 'RMinus $T1 $T2 $T }. -notation "hvbox( ⇧ * [ e ] break T1 ≡ break T2 )" +notation "hvbox( ⇧ * [ e ] break term 46 T1 ≡ break term 46 T2 )" non associative with precedence 45 for @{ 'RLiftStar $e $T1 $T2 }. -notation "hvbox( ⇩ * [ e ] break L1 ≡ break L2 )" +notation "hvbox( ⇩ * [ e ] break term 46 L1 ≡ break term 46 L2 )" non associative with precedence 45 for @{ 'RDropStar $e $L1 $L2 }. -notation "hvbox( T1 break [ d , break e ] ▶* break T2 )" +notation "hvbox( T1 break [ d , break e ] ▶* break term 46 T2 )" non associative with precedence 45 for @{ 'PSubstStar $T1 $d $e $T2 }. -notation "hvbox( L ⊢ break term 90 T1 break [ d , break e ] ▶* break T2 )" +notation "hvbox( L ⊢ break term 46 T1 break [ d , break e ] ▶* break term 46 T2 )" non associative with precedence 45 for @{ 'PSubstStar $L $T1 $d $e $T2 }. -notation "hvbox( L ⊢ break term 90 T1 break [ d , break e ] ▶▶* break T2 )" +notation "hvbox( L ⊢ break term 46 T1 break [ d , break e ] ▶▶* break term 46 T2 )" non associative with precedence 45 for @{ 'PSubstStarAlt $L $T1 $d $e $T2 }. -notation "hvbox( T1 break [ d , break e ] ≡ break T2 )" +notation "hvbox( T1 break [ d , break e ] ≡ break term 46 T2 )" non associative with precedence 45 for @{ 'TSubst $T1 $d $e $T2 }. -notation "hvbox( L ⊢ break term 90 T1 break [ d , break e ] ≡ break T2 )" +notation "hvbox( L ⊢ break term 46 T1 break [ d , break e ] ≡ break term 46 T2 )" non associative with precedence 45 for @{ 'TSubst $L $T1 $d $e $T2 }. @@ -196,27 +196,27 @@ notation "hvbox( T1 break [ d , break e ] ≡≡ break term 46 T2 )" non associative with precedence 45 for @{ 'TSubstAlt $T1 $d $e $T2 }. -notation "hvbox( L ⊢ break term 90 T1 break [ d , break e ] ≡≡ break term 46 T2 )" +notation "hvbox( L ⊢ break term 46 T1 break [ d , break e ] ≡≡ break term 46 T2 )" non associative with precedence 45 for @{ 'TSubstAlt $L $T1 $d $e $T2 }. (* Static typing ************************************************************) -notation "hvbox( L ⊢ break term 90 T ÷ break A )" +notation "hvbox( L ⊢ break term 46 T ÷ break term 46 A )" non associative with precedence 45 for @{ 'AtomicArity $L $T $A }. -notation "hvbox( T1 ÷ ⊑ break T2 )" +notation "hvbox( T1 ÷ ⊑ break term 46 T2 )" non associative with precedence 45 for @{ 'CrSubEqA $T1 $T2 }. -notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 90 T1 • break T2 )" +notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 • break term 46 T2 )" non associative with precedence 45 for @{ 'StaticType $h $L $T1 $T2 }. (* Unwind *******************************************************************) -notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 90 T1 •* break T2 )" +notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 •* break term 46 T2 )" non associative with precedence 45 for @{ 'StaticTypeStar $h $L $T1 $T2 }. @@ -270,45 +270,45 @@ notation "hvbox( L ⊢ break 𝐖𝐇𝐍 [ T ] )" non associative with precedence 45 for @{ 'WHdNormal $L $T }. -notation "hvbox( T1 ➡ break T2 )" +notation "hvbox( T1 ➡ break term 46 T2 )" non associative with precedence 45 for @{ 'PRed $T1 $T2 }. -notation "hvbox( L ⊢ break term 90 T1 ➡ break T2 )" +notation "hvbox( L ⊢ break term 46 T1 ➡ break term 46 T2 )" non associative with precedence 45 for @{ 'PRed $L $T1 $T2 }. -notation "hvbox( L1 ⊢ ➡ break L2 )" +notation "hvbox( L1 ⊢ ➡ break term 46 L2 )" non associative with precedence 45 for @{ 'CPRed $L1 $L2 }. (* Computation **************************************************************) -notation "hvbox( T1 ➡* break T2 )" +notation "hvbox( T1 ➡* break term 46 T2 )" non associative with precedence 45 for @{ 'PRedStar $T1 $T2 }. -notation "hvbox( L ⊢ break term 90 T1 ➡* break T2 )" +notation "hvbox( L ⊢ break term 46 T1 ➡* break term 46 T2 )" non associative with precedence 45 for @{ 'PRedStar $L $T1 $T2 }. -notation "hvbox( L1 ⊢ ➡* break L2 )" +notation "hvbox( L1 ⊢ ➡* break term 46 L2 )" non associative with precedence 45 for @{ 'CPRedStar $L1 $L2 }. -notation "hvbox( L ⊢ break term 90 T1 ➡* break 𝐍 [ T2 ] )" +notation "hvbox( L ⊢ break term 46 T1 ➡* break 𝐍 [ T2 ] )" non associative with precedence 45 for @{ 'PEval $L $T1 $T2 }. -notation "hvbox( ⬇ * T )" +notation "hvbox( ⬇ * term 46 T )" non associative with precedence 45 for @{ 'SN $T }. -notation "hvbox( L ⊢ ⬇ * T )" +notation "hvbox( L ⊢ ⬇ * term 46 T )" non associative with precedence 45 for @{ 'SN $L $T }. -notation "hvbox( L ⊢ ⬇ * * T )" +notation "hvbox( L ⊢ ⬇ * * term 46 T )" non associative with precedence 45 for @{ 'SNStar $L $T }. @@ -316,36 +316,36 @@ notation "hvbox( ⦃ L, break T ⦄ break [ R ] ϵ break 〚 A 〛 )" non associative with precedence 45 for @{ 'InEInt $R $L $T $A }. -notation "hvbox( T1 break [ R ] ⊑ break T2 )" +notation "hvbox( T1 break [ R ] ⊑ break term 46 T2 )" non associative with precedence 45 for @{ 'CrSubEq $T1 $R $T2 }. (* Conversion ***************************************************************) -notation "hvbox( L ⊢ break term 90 T1 ⬌ break T2 )" +notation "hvbox( L ⊢ break term 46 T1 ⬌ break term 46 T2 )" non associative with precedence 45 for @{ 'PConv $L $T1 $T2 }. -notation "hvbox( T1 ⊢ ⬌ break T2 )" +notation "hvbox( T1 ⊢ ⬌ break term 46 T2 )" non associative with precedence 45 for @{ 'CPConv $T1 $T2 }. (* Equivalence **************************************************************) -notation "hvbox( L ⊢ break term 90 T1 ⬌* break T2 )" +notation "hvbox( L ⊢ break term 46 T1 ⬌* break term 46 T2 )" non associative with precedence 45 for @{ 'PConvStar $L $T1 $T2 }. -notation "hvbox( T1 ⊢ ⬌* break T2 )" +notation "hvbox( T1 ⊢ ⬌* break term 46 T2 )" non associative with precedence 45 for @{ 'CPConvStar $T1 $T2 }. (* Dynamic typing ***********************************************************) -notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 90 T1 : break T2 )" +notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 : break term 46 T2 )" non associative with precedence 45 for @{ 'NativeType $h $L $T1 $T2 }. -notation "hvbox( h ⊢ break term 90 L1 : ⊑ break L2 )" +notation "hvbox( h ⊢ break term 46 L1 : ⊑ break term 46 L2 )" non associative with precedence 45 for @{ 'CrSubEqN $h $L1 $L2 }. diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss.ma index 1baa893e4..cc54ed5c0 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss.ma @@ -22,7 +22,7 @@ inductive ltpss: nat → nat → relation lenv ≝ | ltpss_pair : ∀L,I,V. ltpss 0 0 (L. ⓑ{I} V) (L. ⓑ{I} V) | ltpss_tpss2: ∀L1,L2,I,V1,V2,e. ltpss 0 e L1 L2 → L2 ⊢ V1 [0, e] ▶* V2 → - ltpss 0 (e + 1) (L1. ⓑ{I} V1) L2. ⓑ{I} V2 + ltpss 0 (e + 1) (L1. ⓑ{I} V1) (L2. ⓑ{I} V2) | ltpss_tpss1: ∀L1,L2,I,V1,V2,d,e. ltpss d e L1 L2 → L2 ⊢ V1 [d, e] ▶* V2 → ltpss (d + 1) e (L1. ⓑ{I} V1) (L2. ⓑ{I} V2) diff --git a/matita/matita/lib/arithmetics/bigops.ma b/matita/matita/lib/arithmetics/bigops.ma index 447cda347..97bda394d 100644 --- a/matita/matita/lib/arithmetics/bigops.ma +++ b/matita/matita/lib/arithmetics/bigops.ma @@ -70,7 +70,7 @@ notation "\big [ op , nil ]_{ ident j ∈ [a,b[ } f" for @{'bigop ($b-$a) $op $nil (λ${ident j}.((λ${ident j}.true) (${ident j}+$a))) (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}. -(* notation "\big [ op , nil ]_{( term 50) a ≤ ident j < b | p } f" +(* notation "\big [ op , nil ]_{( term 55) a ≤ ident j < b | p } f" with precedence 80 for @{\big[$op,$nil]_{${ident j} < ($b-$a) | ((λ${ident j}.$p) (${ident j}+$a))}((λ${ident j}.$f)(${ident j}+$a))}. *) diff --git a/matita/matita/lib/basics/core_notation.ma b/matita/matita/lib/basics/core_notation.ma index 4eae6c6c3..904adcd52 100644 --- a/matita/matita/lib/basics/core_notation.ma +++ b/matita/matita/lib/basics/core_notation.ma @@ -175,23 +175,23 @@ notation "hvbox(a break \ndivides b)" for @{ 'ndivides $a $b }. notation "hvbox(a break + b)" - left associative with precedence 50 + left associative with precedence 55 for @{ 'plus $a $b }. notation "hvbox(a break - b)" - left associative with precedence 50 + left associative with precedence 55 for @{ 'minus $a $b }. notation "hvbox(a break * b)" - left associative with precedence 55 + left associative with precedence 60 for @{ 'times $a $b }. notation "hvbox(a break \middot b)" - left associative with precedence 55 + left associative with precedence 60 for @{ 'middot $a $b }. notation "hvbox(a break \mod b)" - left associative with precedence 55 + left associative with precedence 60 for @{ 'module $a $b }. notation < "a \frac b" @@ -199,14 +199,14 @@ notation < "a \frac b" for @{ 'divide $a $b }. notation "a \over b" - left associative with precedence 55 + left associative with precedence 60 for @{ 'divide $a $b }. notation "hvbox(a break / b)" - left associative with precedence 55 + left associative with precedence 60 for @{ 'divide $a $b }. -notation "- term 60 a" with precedence 60 +notation "- term 65 a" with precedence 65 for @{ 'uminus $a }. notation "a !" @@ -214,7 +214,7 @@ notation "a !" for @{ 'fact $a }. notation "\sqrt a" - non associative with precedence 60 + non associative with precedence 65 for @{ 'sqrt $a }. notation "hvbox(a break \lor b)" @@ -264,10 +264,10 @@ for @{ 'overlaps $a $b }. (* \between *) notation "hvbox(a break ⊆ b)" non associative with precedence 45 for @{ 'subseteq $a $b }. (* \subseteq *) -notation "hvbox(a break ∩ b)" left associative with precedence 55 +notation "hvbox(a break ∩ b)" left associative with precedence 60 for @{ 'intersects $a $b }. (* \cap *) -notation "hvbox(a break ∪ b)" left associative with precedence 50 +notation "hvbox(a break ∪ b)" left associative with precedence 55 for @{ 'union $a $b }. (* \cup *) notation "hvbox({ term 19 a })" with precedence 90 for @{ 'singl $a}. @@ -279,17 +279,17 @@ notation "hvbox(a break # b)" non associative with precedence 45 for @{ 'apart $a $b}. notation "hvbox(a break \circ b)" - left associative with precedence 55 + left associative with precedence 60 for @{ 'compose $a $b }. -notation < "↓ \ensp a" with precedence 55 for @{ 'downarrow $a }. -notation > "↓ a" with precedence 55 for @{ 'downarrow $a }. +notation < "↓ \ensp a" with precedence 60 for @{ 'downarrow $a }. +notation > "↓ a" with precedence 60 for @{ 'downarrow $a }. -notation "hvbox(U break ↓ V)" non associative with precedence 55 for @{ 'fintersects $U $V }. +notation "hvbox(U break ↓ V)" non associative with precedence 60 for @{ 'fintersects $U $V }. -notation "↑a" with precedence 55 for @{ 'uparrow $a }. +notation "↑a" with precedence 60 for @{ 'uparrow $a }. -notation "hvbox(a break ↑ b)" with precedence 55 for @{ 'funion $a $b }. +notation "hvbox(a break ↑ b)" with precedence 60 for @{ 'funion $a $b }. notation < "term 76 a \sup term 90 b" non associative with precedence 75 for @{ 'exp $a $b}. notation > "a \sup term 90 b" non associative with precedence 75 for @{ 'exp $a $b}. @@ -311,8 +311,8 @@ notation "\ee" with precedence 90 for @{ 'neutral }. (* ⅇ *) notation > "x ⊩ y" with precedence 45 for @{'Vdash2 $x $y ?}. notation > "x ⊩⎽ term 90 c y" with precedence 45 for @{'Vdash2 $x $y $c}. notation "x (⊩ \sub term 90 c) y" with precedence 45 for @{'Vdash2 $x $y $c}. -notation > "⊩ " with precedence 60 for @{'Vdash ?}. -notation "(⊩ \sub term 90 c) " with precedence 60 for @{'Vdash $c}. +notation > "⊩ " with precedence 65 for @{'Vdash ?}. +notation "(⊩ \sub term 90 c) " with precedence 65 for @{'Vdash $c}. notation < "maction (mstyle color #ff0000 (­…­)) (t)" non associative with precedence 90 for @{'hide $t}. diff --git a/matita/matita/lib/basics/lists/list.ma b/matita/matita/lib/basics/lists/list.ma index 2ed7fcc86..ff7fcf80f 100644 --- a/matita/matita/lib/basics/lists/list.ma +++ b/matita/matita/lib/basics/lists/list.ma @@ -162,7 +162,7 @@ let rec length (A:Type[0]) (l:list A) on l ≝ [ nil ⇒ 0 | cons a tl ⇒ S (length A tl)]. -notation "|M|" non associative with precedence 60 for @{'norm $M}. +notation "|M|" non associative with precedence 65 for @{'norm $M}. interpretation "norm" 'norm l = (length ? l). lemma length_tail: ∀A,l. length ? (tail A l) = pred (length ? l). diff --git a/matita/matita/lib/formal_topology/apply_functor.ma b/matita/matita/lib/formal_topology/apply_functor.ma index 41e242caa..55e667540 100644 --- a/matita/matita/lib/formal_topology/apply_functor.ma +++ b/matita/matita/lib/formal_topology/apply_functor.ma @@ -21,11 +21,11 @@ record Fo (C1,C2:CAT2) (F:arrows3 CAT2 C1 C2) : Type[2] ≝ { FP: map_objs2 ?? F F1 =_\ID F2 }. -notation "ℱ\sub 1 x" non associative with precedence 60 for @{'F1 $x}. +notation "ℱ\sub 1 x" non associative with precedence 65 for @{'F1 $x}. notation > "ℱ_1" non associative with precedence 90 for @{F1 ???}. interpretation "F1" 'F1 x = (F1 ??? x). -notation "ℱ\sub 2 x" non associative with precedence 60 for @{'F2 $x}. +notation "ℱ\sub 2 x" non associative with precedence 65 for @{'F2 $x}. notation > "ℱ_2" non associative with precedence 90 for @{F2 ???}. interpretation "F2" 'F2 x = (F2 ??? x). @@ -42,11 +42,11 @@ record Fm_c (C1,C2:CAT2) (F:arrows3 CAT2 C1 C2) (X,Y:Fo ?? F) : Type[2] ≝ { FmP: REW ?? F X Y (map_arrows2 ?? F ?? Fm1) = Fm2 }. -notation "ℳ\sub 1 x" non associative with precedence 60 for @{'Fm1 $x}. +notation "ℳ\sub 1 x" non associative with precedence 65 for @{'Fm1 $x}. notation > "ℳ_1" non associative with precedence 90 for @{Fm1 ?????}. interpretation "Fm1" 'Fm1 x = (Fm1 ????? x). -notation "ℳ\sub 2 x" non associative with precedence 60 for @{'Fm2 $x}. +notation "ℳ\sub 2 x" non associative with precedence 65 for @{'Fm2 $x}. notation > "ℳ_2" non associative with precedence 90 for @{Fm2 ?????}. interpretation "Fm2" 'Fm2 x = (Fm2 ????? x). diff --git a/matita/matita/lib/formal_topology/categories.ma b/matita/matita/lib/formal_topology/categories.ma index 68a02e964..f5cad55fe 100644 --- a/matita/matita/lib/formal_topology/categories.ma +++ b/matita/matita/lib/formal_topology/categories.ma @@ -128,7 +128,7 @@ interpretation "setoid3 symmetry" 'invert r = (sym3 ???? r). interpretation "setoid2 symmetry" 'invert r = (sym2 ???? r). interpretation "setoid1 symmetry" 'invert r = (sym1 ???? r). interpretation "setoid symmetry" 'invert r = (sym ???? r). -notation ".= r" with precedence 50 for @{'trans $r}. +notation ".= r" with precedence 55 for @{'trans $r}. interpretation "trans3" 'trans r = (trans3 ????? r). interpretation "trans2" 'trans r = (trans2 ????? r). interpretation "trans1" 'trans r = (trans1 ????? r). @@ -244,7 +244,7 @@ definition fi': ∀A,B:CPROP. A = B → B → A. #A #B #e #b @(fi ?? e) assumption. qed. -notation ". r" with precedence 50 for @{'fi $r}. +notation ". r" with precedence 55 for @{'fi $r}. interpretation "fi" 'fi r = (fi' ?? r). definition and_morphism: binary_morphism1 CPROP CPROP CPROP. @@ -279,7 +279,7 @@ definition if_morphism: binary_morphism1 CPROP CPROP CPROP. | @(fi ?? e1) @f @(if ?? e) assumption]] qed. (* -notation > "hvbox(a break ∘ b)" left associative with precedence 55 for @{ comp ??? $a $b }. +notation > "hvbox(a break ∘ b)" left associative with precedence 60 for @{ comp ??? $a $b }. *) record category : Type[1] ≝ { objs:> Type[0]; @@ -292,7 +292,7 @@ record category : Type[1] ≝ { id_neutral_right: ∀o1,o2. ∀a: arrows o1 o2. comp ??? a (id o2) =_0 a }. (* -notation "hvbox(a break ∘ b)" left associative with precedence 55 for @{ 'compose $a $b }. +notation "hvbox(a break ∘ b)" left associative with precedence 60 for @{ 'compose $a $b }. *) record category1 : Type[2] ≝ { objs1:> Type[1]; @@ -360,8 +360,8 @@ record functor2 (C1: category2) (C2: category2) : Type[3] ≝ ∀o1,o2,o3.∀f1:arrows2 ? o1 o2.∀f2:arrows2 ? o2 o3. map_arrows2 ?? (f2 ∘ f1) = map_arrows2 ?? f2 ∘ map_arrows2 ?? f1}. -notation > "F⎽⇒ x" left associative with precedence 60 for @{'map_arrows2 $F $x}. -notation "F\sub⇒ x" left associative with precedence 60 for @{'map_arrows2 $F $x}. +notation > "F⎽⇒ x" left associative with precedence 65 for @{'map_arrows2 $F $x}. +notation "F\sub⇒ x" left associative with precedence 65 for @{'map_arrows2 $F $x}. interpretation "map_arrows2" 'map_arrows2 F x = (fun12 ?? (map_arrows2 ?? F ??) x). definition functor2_setoid: category2 → category2 → setoid3. diff --git a/matita/matita/lib/formal_topology/o-algebra.ma b/matita/matita/lib/formal_topology/o-algebra.ma index f84249343..496485975 100644 --- a/matita/matita/lib/formal_topology/o-algebra.ma +++ b/matita/matita/lib/formal_topology/o-algebra.ma @@ -100,11 +100,11 @@ for @{ 'overlap $a $b}. interpretation "o-algebra overlap" 'overlap a b = (fun21 ??? (oa_overlap ?) a b). notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∧) \below (\emsp) \nbsp term 90 p)" -non associative with precedence 50 for @{ 'oa_meet $p }. +non associative with precedence 55 for @{ 'oa_meet $p }. notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∧) \below (ident i ∈  I) break term 90 p)" -non associative with precedence 50 for @{ 'oa_meet_mk (λ${ident i}:$I.$p) }. +non associative with precedence 55 for @{ 'oa_meet_mk (λ${ident i}:$I.$p) }. -notation > "hovbox(∧ f)" non associative with precedence 60 +notation > "hovbox(∧ f)" non associative with precedence 65 for @{ 'oa_meet $f }. interpretation "o-algebra meet" 'oa_meet f = (fun12 ?? (oa_meet ??) f). @@ -112,11 +112,11 @@ interpretation "o-algebra meet with explicit function" 'oa_meet_mk f = (fun12 ?? (oa_meet ??) (mk_unary_morphism1 ?? f ?)). notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∨) \below (\emsp) \nbsp term 90 p)" -non associative with precedence 50 for @{ 'oa_join $p }. +non associative with precedence 55 for @{ 'oa_join $p }. notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∨) \below (ident i ∈  I) break term 90 p)" -non associative with precedence 50 for @{ 'oa_join_mk (λ${ident i}:$I.$p) }. +non associative with precedence 55 for @{ 'oa_join_mk (λ${ident i}:$I.$p) }. -notation > "hovbox(∨ f)" non associative with precedence 60 +notation > "hovbox(∨ f)" non associative with precedence 65 for @{ 'oa_join $f }. interpretation "o-algebra join" 'oa_join f = (fun12 ?? (oa_join ??) f). @@ -166,7 +166,7 @@ non associative with precedence 49 for @{ 'oa_join_mk (λ${ident i}:$I.$p) }. notation < "hovbox(a ∨ b)" left associative with precedence 49 for @{ 'oa_join_mk (λ${ident i}:$_.match $i with [ true ⇒ $a | false ⇒ $b ]) }. -notation > "hovbox(∨ f)" non associative with precedence 59 +notation > "hovbox(∨ f)" non associative with precedence 64 for @{ 'oa_join $f }. notation > "hovbox(a ∨ b)" left associative with precedence 49 for @{ 'oa_join (mk_unary_morphism BOOL ? (λx__:bool.match x__ with [ true ⇒ $a | false ⇒ $b ]) (IF_THEN_ELSE_p ? $a $b)) }. diff --git a/matita/matita/lib/formal_topology/r-o-basic_pairs.ma b/matita/matita/lib/formal_topology/r-o-basic_pairs.ma index 76d077cfa..0218ed835 100644 --- a/matita/matita/lib/formal_topology/r-o-basic_pairs.ma +++ b/matita/matita/lib/formal_topology/r-o-basic_pairs.ma @@ -93,7 +93,7 @@ lemma curry: ∀A,B,C.(A × B ⇒_1 C) → A → (B ⇒_1 C). | intros; apply (#‡e); ] qed. -notation < "F x" left associative with precedence 60 for @{'map_arrows $F $x}. +notation < "F x" left associative with precedence 65 for @{'map_arrows $F $x}. interpretation "map arrows 2" 'map_arrows F x = (fun12 ? ? (map_arrows2 ? ? F ? ?) x). definition preserve_sup : ∀S,T.∀ f:Ω^S ⇒_1 Ω^T. CProp[1]. diff --git a/matita/matita/lib/formal_topology/subsets.ma b/matita/matita/lib/formal_topology/subsets.ma index 15bfb98d3..8bacd2a55 100644 --- a/matita/matita/lib/formal_topology/subsets.ma +++ b/matita/matita/lib/formal_topology/subsets.ma @@ -164,16 +164,16 @@ definition big_union: ∀A:SET.∀I:SET.(I ⇒_2 Ω^A) ⇒_2 Ω^A. qed. notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (⋃) \below (\emsp) term 90 p)" -non associative with precedence 50 for @{ 'bigcup $p }. +non associative with precedence 55 for @{ 'bigcup $p }. notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (⋃) \below (ident i ∈  I) break term 90 p)" -non associative with precedence 50 for @{ 'bigcup_mk (λ${ident i}:$I.$p) }. -notation > "hovbox(⋃ f)" non associative with precedence 60 for @{ 'bigcup $f }. +non associative with precedence 55 for @{ 'bigcup_mk (λ${ident i}:$I.$p) }. +notation > "hovbox(⋃ f)" non associative with precedence 65 for @{ 'bigcup $f }. notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (⋂) \below (\emsp) term 90 p)" -non associative with precedence 50 for @{ 'bigcap $p }. +non associative with precedence 55 for @{ 'bigcap $p }. notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (⋂) \below (ident i ∈  I) break term 90 p)" -non associative with precedence 50 for @{ 'bigcap_mk (λ${ident i}:$I.$p) }. -notation > "hovbox(⋂ f)" non associative with precedence 60 for @{ 'bigcap $f }. +non associative with precedence 55 for @{ 'bigcap_mk (λ${ident i}:$I.$p) }. +notation > "hovbox(⋂ f)" non associative with precedence 65 for @{ 'bigcap $f }. interpretation "bigcup" 'bigcup f = (fun12 ?? (big_union ??) f). interpretation "bigcap" 'bigcap f = (fun12 ?? (big_intersects ??) f). diff --git a/matita/matita/lib/lambda/lambda_notation.ma b/matita/matita/lib/lambda/lambda_notation.ma index 8063634d0..e9e84c828 100644 --- a/matita/matita/lib/lambda/lambda_notation.ma +++ b/matita/matita/lib/lambda/lambda_notation.ma @@ -23,18 +23,18 @@ notation "hvbox(a break (≅ ^ term 90 c) b)" non associative with precedence 45 for @{'Eq1 $c $a $b}. -notation "hbox(! term 50 a)" - non associative with precedence 50 +notation "hbox(! term 55 a)" + non associative with precedence 55 for @{'Invariant $a}. -notation "hbox((! ^ term 90 b) term 50 a)" - non associative with precedence 50 +notation "hbox((! ^ term 90 b) term 55 a)" + non associative with precedence 55 for @{'Invariant1 $a $b}. (* lifting, substitution *) notation "hvbox(↑ [ p break , k ] break t)" - non associative with precedence 50 + non associative with precedence 55 for @{'Lift1 $p $k $t}. notation "hvbox(M break [ / l ])" @@ -58,49 +58,49 @@ notation "hvbox(G break ⊢ A break ÷ B)" (* interpretations *) notation "hvbox(║T║)" - non associative with precedence 50 + non associative with precedence 55 for @{'IInt $T}. notation "hvbox(║T║ break _ [E])" - non associative with precedence 50 + non associative with precedence 55 for @{'IInt1 $T $E}. notation "hvbox(║T║ break _ [E1 break , E2])" - non associative with precedence 50 + non associative with precedence 55 for @{'IInt2 $T $E1 $E2}. notation "hvbox(║T║ * break _ [E])" - non associative with precedence 50 + non associative with precedence 55 for @{'IIntS1 $T $E}. notation "hvbox(〚T〛)" - non associative with precedence 50 + non associative with precedence 55 for @{'EInt $T}. notation "hvbox(〚T〛 break _ [E])" - non associative with precedence 50 + non associative with precedence 55 for @{'EInt1 $T $E}. notation "hvbox(〚T〛 break _ [E1 break , E2])" - non associative with precedence 50 + non associative with precedence 55 for @{'EInt2 $T $E1 $E2}. notation "hvbox(《T》)" - non associative with precedence 50 + non associative with precedence 55 for @{'XInt $T}. notation "hvbox(《T》 break _ [E])" - non associative with precedence 50 + non associative with precedence 55 for @{'XInt1 $T $E}. notation "hvbox(《T》 break _ [E1 break , E2])" - non associative with precedence 50 + non associative with precedence 55 for @{'XInt2 $T $E1 $E2}. notation "hvbox(𝕂{G})" - non associative with precedence 50 + non associative with precedence 55 for @{'IK $G}. notation "hvbox(𝕂{T} break _ [G])" - non associative with precedence 50 + non associative with precedence 55 for @{'IK $T $G}. diff --git a/matita/matita/lib/lambdaN/lambda_notation.ma b/matita/matita/lib/lambdaN/lambda_notation.ma index 596424938..57c02e03a 100644 --- a/matita/matita/lib/lambdaN/lambda_notation.ma +++ b/matita/matita/lib/lambdaN/lambda_notation.ma @@ -23,18 +23,18 @@ notation "hvbox(a break (≅ ^ term 90 c) b)" non associative with precedence 45 for @{'Eq1 $c $a $b}. -notation "hbox(! term 50 a)" - non associative with precedence 50 +notation "hbox(! term 55 a)" + non associative with precedence 55 for @{'Invariant $a}. -notation "hbox((! ^ term 90 b) term 50 a)" - non associative with precedence 50 +notation "hbox((! ^ term 90 b) term 55 a)" + non associative with precedence 55 for @{'Invariant1 $a $b}. (* lifting, substitution *) notation "hvbox(↑ [ p break , k ] break t)" - non associative with precedence 50 + non associative with precedence 55 for @{'Lift1 $p $k $t}. notation "hvbox(M break [ / l ])" @@ -58,37 +58,37 @@ notation "hvbox(G break ⊢ A break ÷ B)" (* interpretations *) notation "hvbox(║T║)" - non associative with precedence 50 + non associative with precedence 55 for @{'IInt $T}. notation "hvbox(║T║ break _ [E])" - non associative with precedence 50 + non associative with precedence 55 for @{'IInt1 $T $E}. notation "hvbox(║T║ break _ [E1 break , E2])" - non associative with precedence 50 + non associative with precedence 55 for @{'IInt2 $T $E1 $E2}. notation "hvbox(〚T〛)" - non associative with precedence 50 + non associative with precedence 55 for @{'EInt $T}. notation "hvbox(〚T〛 break _ [E])" - non associative with precedence 50 + non associative with precedence 55 for @{'EInt1 $T $E}. notation "hvbox(〚T〛 break _ [E1 break , E2])" - non associative with precedence 50 + non associative with precedence 55 for @{'EInt2 $T $E1 $E2}. notation "hvbox(《T》)" - non associative with precedence 50 + non associative with precedence 55 for @{'XInt $T}. notation "hvbox(《T》 break _ [E])" - non associative with precedence 50 + non associative with precedence 55 for @{'XInt1 $T $E}. notation "hvbox(《T》 break _ [E1 break , E2])" - non associative with precedence 50 + non associative with precedence 55 for @{'XInt2 $T $E1 $E2}. diff --git a/matita/matita/lib/re/lang.ma b/matita/matita/lib/re/lang.ma index 172693924..aedf4c131 100644 --- a/matita/matita/lib/re/lang.ma +++ b/matita/matita/lib/re/lang.ma @@ -27,7 +27,7 @@ interpretation "epsilon" 'epsilon = (nil ?). (* concatenation *) definition cat : ∀S,l1,l2,w.Prop ≝ λS.λl1,l2.λw:word S.∃w1,w2.w1 @ w2 = w ∧ l1 w1 ∧ l2 w2. -notation "a · b" non associative with precedence 60 for @{ 'middot $a $b}. +notation "a · b" non associative with precedence 65 for @{ 'middot $a $b}. interpretation "cat lang" 'middot a b = (cat ? a b). let rec flatten (S : DeqSet) (l : list (word S)) on l : word S ≝ diff --git a/matita/matita/lib/re/moves.ma b/matita/matita/lib/re/moves.ma index 1372b4976..582531777 100644 --- a/matita/matita/lib/re/moves.ma +++ b/matita/matita/lib/re/moves.ma @@ -110,7 +110,7 @@ theorem move_ok: ] qed. -notation > "x ↦* E" non associative with precedence 60 for @{moves ? $x $E}. +notation > "x ↦* E" non associative with precedence 65 for @{moves ? $x $E}. let rec moves (S : DeqSet) w e on w : pre S ≝ match w with [ nil ⇒ e diff --git a/matita/matita/lib/re/re.ma b/matita/matita/lib/re/re.ma index 9b6378846..60c200e6c 100644 --- a/matita/matita/lib/re/re.ma +++ b/matita/matita/lib/re/re.ma @@ -342,7 +342,7 @@ then, we just have •(i1+i2) = •(i1)⊕ •(i2). *) definition lo ≝ λS:DeqSet.λa,b:pre S.〈\fst a + \fst b,\snd a ∨ \snd b〉. -notation "a ⊕ b" left associative with precedence 60 for @{'oplus $a $b}. +notation "a ⊕ b" left associative with precedence 65 for @{'oplus $a $b}. interpretation "oplus" 'oplus a b = (lo ? a b). lemma lo_def: ∀S.∀i1,i2:pitem S.∀b1,b2. 〈i1,b1〉⊕〈i2,b2〉=〈i1+i2,b1∨b2〉. @@ -368,7 +368,7 @@ Let us come to the formalized definitions: definition pre_concat_r ≝ λS:DeqSet.λi:pitem S.λe:pre S. match e with [ mk_Prod i1 b ⇒ 〈i · i1, b〉]. -notation "i ◃ e" left associative with precedence 60 for @{'lhd $i $e}. +notation "i ◃ e" left associative with precedence 65 for @{'lhd $i $e}. interpretation "pre_concat_r" 'lhd i e = (pre_concat_r ? i e). (* The behaviour of ◃ is summarized by the following, easy lemma: *) @@ -397,10 +397,10 @@ definition pre_concat_l ≝ λS:DeqSet.λbcast:∀S:DeqSet.pitem S → pre S.λe ] ]. -notation "a ▹ b" left associative with precedence 60 for @{'tril eclose $a $b}. +notation "a ▹ b" left associative with precedence 65 for @{'tril eclose $a $b}. interpretation "item-pre concat" 'tril op a b = (pre_concat_l ? op a b). -notation "•" non associative with precedence 60 for @{eclose ?}. +notation "•" non associative with precedence 65 for @{eclose ?}. (* We are ready to give the formal definition of the broadcasting operation. *) @@ -414,7 +414,7 @@ let rec eclose (S: DeqSet) (i: pitem S) on i : pre S ≝ | pc i1 i2 ⇒ •i1 ▹ i2 | pk i ⇒ 〈(\fst (•i))^*,true〉]. -notation "• x" non associative with precedence 60 for @{'eclose $x}. +notation "• x" non associative with precedence 65 for @{'eclose $x}. interpretation "eclose" 'eclose x = (eclose ? x). (* Here are a few simple properties of ▹ and •(-) *) diff --git a/matita/matita/lib/re/reb.ma b/matita/matita/lib/re/reb.ma index 79a74c24d..e1d85641f 100644 --- a/matita/matita/lib/re/reb.ma +++ b/matita/matita/lib/re/reb.ma @@ -48,7 +48,7 @@ notation > "a ^ *" non associative with precedence 90 for @{ 'pk $a}. interpretation "star" 'pk a = (k ? a). interpretation "or" 'plus a b = (o ? a b). -notation "a · b" non associative with precedence 60 for @{ 'pc $a $b}. +notation "a · b" non associative with precedence 65 for @{ 'pc $a $b}. interpretation "cat" 'pc a b = (c ? a b). (* to get rid of \middot @@ -134,7 +134,7 @@ interpretation "patom" 'ps a = (ps ? a). interpretation "pepsilon" 'epsilon = (pe ?). interpretation "pempty" 'empty = (pz ?). -notation > "| e |" non associative with precedence 65 for @{forget ? $e}. +notation > "| e |" non associative with precedence 66 for @{forget ? $e}. let rec forget (S: Alpha) (l : pitem S) on l: re S ≝ match l with [ pz ⇒ ∅ @@ -195,7 +195,7 @@ lemma true_to_epsilon : ∀S.∀e:pre S. \snd e = true → [ ] ∈ e. qed. definition lo ≝ λS:Alpha.λa,b:pre S.〈\fst a + \fst b,\snd a || \snd b〉. -notation "a ⊕ b" left associative with precedence 60 for @{'oplus $a $b}. +notation "a ⊕ b" left associative with precedence 65 for @{'oplus $a $b}. interpretation "oplus" 'oplus a b = (lo ? a b). lemma lo_def: ∀S.∀i1,i2:pitem S.∀b1,b2. 〈i1,b1〉⊕〈i2,b2〉=〈i1+i2,b1||b2〉. @@ -216,9 +216,9 @@ definition lift ≝ λf:∀S.pitem S →pre S.λS.λe:pre S. match e with [ pair i b ⇒ 〈\fst (f S i), \snd (f S i) || b〉]. -notation < "a ⊙ b" left associative with precedence 60 for @{'lc $op $a $b}. +notation < "a ⊙ b" left associative with precedence 65 for @{'lc $op $a $b}. interpretation "lc" 'lc op a b = (lc ? op a b). -notation > "a ⊙ b" left associative with precedence 60 for @{'lc (lift eclose) $a $b}. +notation > "a ⊙ b" left associative with precedence 65 for @{'lc (lift eclose) $a $b}. definition lk ≝ λS:Alpha.λbcast:∀S:Alpha.∀E:pitem S.pre S.λe:pre S. match e with @@ -234,7 +234,7 @@ interpretation "lk" 'lk op a = (lk ? op a). notation > "a^⊛" non associative with precedence 90 for @{'lk eclose $a}. -notation > "•" non associative with precedence 60 for @{eclose ?}. +notation > "•" non associative with precedence 65 for @{eclose ?}. let rec eclose (S: Alpha) (i: pitem S) on i : pre S ≝ match i with [ pz ⇒ 〈 ∅, false 〉 @@ -245,9 +245,9 @@ let rec eclose (S: Alpha) (i: pitem S) on i : pre S ≝ | pc E1 E2 ⇒ •E1 ⊙ 〈E2,false〉 | pk E ⇒ 〈(\fst(•E))^*,true〉]. -notation < "• x" non associative with precedence 60 for @{'eclose $x}. +notation < "• x" non associative with precedence 65 for @{'eclose $x}. interpretation "eclose" 'eclose x = (eclose ? x). -notation > "• x" non associative with precedence 60 for @{'eclose $x}. +notation > "• x" non associative with precedence 65 for @{'eclose $x}. definition reclose ≝ lift eclose. interpretation "reclose" 'eclose x = (reclose ? x). @@ -545,7 +545,7 @@ ntheorem bull_true_epsilon : ∀S.∀e:pitem S. \snd (•e) = true ↔ [ ] ∈ | STOP notation > "\move term 90 x term 90 E" -non associative with precedence 60 for @{move ? $x $E}. +non associative with precedence 65 for @{move ? $x $E}. nlet rec move (S: Alpha) (x:S) (E: pitem S) on E : pre S ≝ match E with [ pz ⇒ 〈 ∅, false 〉 @@ -555,8 +555,8 @@ nlet rec move (S: Alpha) (x:S) (E: pitem S) on E : pre S ≝ | po e1 e2 ⇒ \move x e1 ⊕ \move x e2 | pc e1 e2 ⇒ \move x e1 ⊙ \move x e2 | pk e ⇒ (\move x e)^⊛ ]. -notation < "\move\shy x\shy E" non associative with precedence 60 for @{'move $x $E}. -notation > "\move term 90 x term 90 E" non associative with precedence 60 for @{'move $x $E}. +notation < "\move\shy x\shy E" non associative with precedence 65 for @{'move $x $E}. +notation > "\move term 90 x term 90 E" non associative with precedence 65 for @{'move $x $E}. interpretation "move" 'move x E = (move ? x E). ndefinition rmove ≝ λS:Alpha.λx:S.λe:pre S. \move x (\fst e). @@ -626,7 +626,7 @@ ntheorem move_ok: nqed. -notation > "x ↦* E" non associative with precedence 60 for @{move_star ? $x $E}. +notation > "x ↦* E" non associative with precedence 65 for @{move_star ? $x $E}. nlet rec move_star (S : decidable) w E on w : bool × (pre S) ≝ match w with [ nil ⇒ E diff --git a/matita/matita/library/algebra/finite_groups.ma b/matita/matita/library/algebra/finite_groups.ma index 30408be37..dba8ff895 100644 --- a/matita/matita/library/algebra/finite_groups.ma +++ b/matita/matita/library/algebra/finite_groups.ma @@ -41,7 +41,7 @@ record finite_enumerable_SemiGroup : Type≝ interpretation "Finite_enumerable representation" 'repr S i = (repr S (is_finite_enumerable S) i). -notation "hvbox(\iota e)" with precedence 60 +notation "hvbox(\iota e)" with precedence 65 for @{ 'index_of_finite_enumerable_semigroup $e }. interpretation "Index_of_finite_enumerable representation" diff --git a/matita/matita/library/dama/bishop_set_rewrite.ma b/matita/matita/library/dama/bishop_set_rewrite.ma index 55964d684..88e4c3d37 100644 --- a/matita/matita/library/dama/bishop_set_rewrite.ma +++ b/matita/matita/library/dama/bishop_set_rewrite.ma @@ -19,7 +19,7 @@ coercion eq_sym. lemma eq_trans:∀E:bishop_set.∀x,z,y:E.x ≈ y → y ≈ z → x ≈ z ≝ λE,x,y,z.eq_trans_ E x z y. -notation > "'Eq'≈" non associative with precedence 50 +notation > "'Eq'≈" non associative with precedence 55 for @{'eqrewrite}. interpretation "eq_rew" 'eqrewrite = (eq_trans ? ? ?). @@ -34,9 +34,9 @@ intros (E z y x Exy Lxz); apply (le_transitive ??? Lxz); intro Xyz; apply Exy; left; assumption; qed. -notation > "'Le'≪" non associative with precedence 50 for @{'lerewritel}. +notation > "'Le'≪" non associative with precedence 55 for @{'lerewritel}. interpretation "le_rewl" 'lerewritel = (le_rewl ? ? ?). -notation > "'Le'≫" non associative with precedence 50 for @{'lerewriter}. +notation > "'Le'≫" non associative with precedence 55 for @{'lerewriter}. interpretation "le_rewr" 'lerewriter = (le_rewr ? ? ?). lemma ap_rewl: ∀A:bishop_set.∀x,z,y:A. x ≈ y → y # z → x # z. @@ -49,9 +49,9 @@ intros (A x z y Exy Azy); apply bs_symmetric; apply (ap_rewl ???? Exy); apply bs_symmetric; assumption; qed. -notation > "'Ap'≪" non associative with precedence 50 for @{'aprewritel}. +notation > "'Ap'≪" non associative with precedence 55 for @{'aprewritel}. interpretation "ap_rewl" 'aprewritel = (ap_rewl ? ? ?). -notation > "'Ap'≫" non associative with precedence 50 for @{'aprewriter}. +notation > "'Ap'≫" non associative with precedence 55 for @{'aprewriter}. interpretation "ap_rewr" 'aprewriter = (ap_rewr ? ? ?). lemma exc_rewl: ∀A:ordered_set.∀x,z,y:A. x ≈ y → y ≰ z → x ≰ z. @@ -64,9 +64,9 @@ intros (A x z y Exy Azy); cases (exc_cotransitive ??x Azy); [assumption] cases (Exy); left; assumption; qed. -notation > "'Ex'≪" non associative with precedence 50 for @{'ordered_setrewritel}. +notation > "'Ex'≪" non associative with precedence 55 for @{'ordered_setrewritel}. interpretation "exc_rewl" 'ordered_setrewritel = (exc_rewl ? ? ?). -notation > "'Ex'≫" non associative with precedence 50 for @{'ordered_setrewriter}. +notation > "'Ex'≫" non associative with precedence 55 for @{'ordered_setrewriter}. interpretation "exc_rewr" 'ordered_setrewriter = (exc_rewr ? ? ?). (* @@ -80,8 +80,8 @@ intros (A x y z E H); split; cases H; [apply (Le≪ ? (eq_sym ??? E));| apply (Ap≪ ? E);] assumption; qed. -notation > "'Lt'≪" non associative with precedence 50 for @{'ltrewritel}. +notation > "'Lt'≪" non associative with precedence 55 for @{'ltrewritel}. interpretation "lt_rewl" 'ltrewritel = (lt_rewl ? ? ?). -notation > "'Lt'≫" non associative with precedence 50 for @{'ltrewriter}. +notation > "'Lt'≫" non associative with precedence 55 for @{'ltrewriter}. interpretation "lt_rewr" 'ltrewriter = (lt_rewr ? ? ?). *) diff --git a/matita/matita/library/dama/russell_support.ma b/matita/matita/library/dama/russell_support.ma index fc75b76b4..126c94381 100644 --- a/matita/matita/library/dama/russell_support.ma +++ b/matita/matita/library/dama/russell_support.ma @@ -17,7 +17,7 @@ include "logic/cprop_connectives.ma". definition hide ≝ λT:Type.λx:T.x. -notation < "\blacksquare" non associative with precedence 50 for @{'hide}. +notation < "\blacksquare" non associative with precedence 55 for @{'hide}. interpretation "hide" 'hide = (hide ? ?). interpretation "hide2" 'hide = (hide ? ? ?). diff --git a/matita/matita/library/dama/uniform.ma b/matita/matita/library/dama/uniform.ma index d6637a85d..137b63ef3 100644 --- a/matita/matita/library/dama/uniform.ma +++ b/matita/matita/library/dama/uniform.ma @@ -33,7 +33,7 @@ definition invert_bs_relation ≝ λC:bishop_set.λU:C squareB → Prop. λx:C squareB. U 〈\snd x,\fst x〉. -notation > "\inv" with precedence 60 for @{ 'invert_symbol }. +notation > "\inv" with precedence 65 for @{ 'invert_symbol }. interpretation "relation invertion" 'invert a = (invert_bs_relation ? a). interpretation "relation invertion" 'invert_symbol = (invert_bs_relation ?). interpretation "relation invertion" 'invert_appl a x = (invert_bs_relation ? a x). diff --git a/matita/matita/library/datatypes/categories.ma b/matita/matita/library/datatypes/categories.ma index b9e365c7e..e123a8772 100644 --- a/matita/matita/library/datatypes/categories.ma +++ b/matita/matita/library/datatypes/categories.ma @@ -84,7 +84,7 @@ interpretation "setoid1 eq" 'eq t x y = (eq_rel1 ? (eq1 t) x y). interpretation "setoid eq" 'eq t x y = (eq_rel ? (eq t) x y). interpretation "setoid1 symmetry" 'invert r = (sym1 ???? r). interpretation "setoid symmetry" 'invert r = (sym ???? r). -notation ".= r" with precedence 50 for @{'trans $r}. +notation ".= r" with precedence 55 for @{'trans $r}. interpretation "trans1" 'trans r = (trans1 ????? r). interpretation "trans" 'trans r = (trans ????? r). @@ -127,7 +127,7 @@ definition if': ∀A,B:CPROP. A = B → A → B. intros; apply (if ?? H); assumption. qed. -notation ". r" with precedence 50 for @{'if $r}. +notation ". r" with precedence 55 for @{'if $r}. interpretation "if" 'if r = (if' ?? r). definition and_morphism: binary_morphism1 CPROP CPROP CPROP. diff --git a/matita/matita/library/demo/power_derivative.ma b/matita/matita/library/demo/power_derivative.ma index a425dfcc3..3512ad6fe 100644 --- a/matita/matita/library/demo/power_derivative.ma +++ b/matita/matita/library/demo/power_derivative.ma @@ -213,11 +213,11 @@ interpretation "Rderivative" 'derivative f = (derivative f). * Any file that includes this one can not use 'x' as an identifier *) notation "hvbox('X' \sup n)" - non associative with precedence 60 + non associative with precedence 65 for @{ 'monomio $n }. notation "hvbox('X')" - non associative with precedence 60 + non associative with precedence 65 for @{ 'monomio 1 }. interpretation "Rmonomio" 'monomio n = (monomio n). diff --git a/matita/matita/library/didactic/exercises/duality.ma b/matita/matita/library/didactic/exercises/duality.ma index 14927653e..f967a416b 100644 --- a/matita/matita/library/didactic/exercises/duality.ma +++ b/matita/matita/library/didactic/exercises/duality.ma @@ -219,7 +219,7 @@ let rec negate (F: Formula) on F : Formula ≝ *) definition equiv ≝ λF1,F2. ∀v.[[ F1 ]]v = [[ F2 ]]v. notation "hvbox(a \nbsp break mstyle color #0000ff (≡) \nbsp b)" non associative with precedence 45 for @{ 'equivF $a $b }. -notation > "a ≡ b" non associative with precedence 50 for @{ equiv $a $b }. +notation > "a ≡ b" non associative with precedence 55 for @{ equiv $a $b }. interpretation "equivalence for Formulas" 'equivF a b = (equiv a b). lemma equiv_rewrite : ∀F1,F2,F3. F1 ≡ F2 → F1 ≡ F3 → F2 ≡ F3. intros; intro; rewrite < H; rewrite < H1; reflexivity. qed. lemma equiv_sym : ∀a,b.a ≡ b → b ≡ a. intros 4;symmetry;apply H;qed. diff --git a/matita/matita/library/didactic/exercises/natural_deduction_theories.ma b/matita/matita/library/didactic/exercises/natural_deduction_theories.ma index 9768e26e2..7d5d89378 100644 --- a/matita/matita/library/didactic/exercises/natural_deduction_theories.ma +++ b/matita/matita/library/didactic/exercises/natural_deduction_theories.ma @@ -197,8 +197,8 @@ interpretation "=" 'my_eq x y = (eq x y). interpretation "S" 'my_S x = (S x). interpretation "O" 'my_O = O. -notation "x + y" non associative with precedence 50 for @{'my_plus $x $y}. -notation "x * y" non associative with precedence 55 for @{'my_mult $x $y}. +notation "x + y" non associative with precedence 55 for @{'my_plus $x $y}. +notation "x * y" non associative with precedence 60 for @{'my_mult $x $y}. notation "x = y" non associative with precedence 45 for @{'my_eq $x $y}. notation > "'S' x" non associative with precedence 40 for @{'my_S $x}. notation < "'S'  x" non associative with precedence 40 for @{'my_S $x}. diff --git a/matita/matita/library/didactic/exercises/shannon.ma b/matita/matita/library/didactic/exercises/shannon.ma index 78504385f..c3aa746c8 100644 --- a/matita/matita/library/didactic/exercises/shannon.ma +++ b/matita/matita/library/didactic/exercises/shannon.ma @@ -114,7 +114,7 @@ notation > "t [ term 90 a / term 90 b]" non associative with precedence 19 for @ interpretation "Substitution for Formula" 'substitution b a t = (subst b a t). definition equiv ≝ λF1,F2. ∀v.[[ F1 ]]v = [[ F2 ]]v. notation "hvbox(a \nbsp break mstyle color #0000ff (≡) \nbsp b)" non associative with precedence 45 for @{ 'equivF $a $b }. -notation > "a ≡ b" non associative with precedence 50 for @{ equiv $a $b }. +notation > "a ≡ b" non associative with precedence 55 for @{ equiv $a $b }. interpretation "equivalence for Formulas" 'equivF a b = (equiv a b). lemma min_1_sem: ∀F,v.min 1 [[ F ]]v = [[ F ]]v. intros; cases (sem_bool F v); rewrite > H; reflexivity; qed. lemma max_0_sem: ∀F,v.max [[ F ]]v 0 = [[ F ]]v. intros; cases (sem_bool F v); rewrite > H; reflexivity; qed. diff --git a/matita/matita/library/didactic/exercises/substitution.ma b/matita/matita/library/didactic/exercises/substitution.ma index db83cfef8..e55569a4b 100644 --- a/matita/matita/library/didactic/exercises/substitution.ma +++ b/matita/matita/library/didactic/exercises/substitution.ma @@ -298,7 +298,7 @@ notation > "t [ term 90 a / term 90 b]" non associative with precedence 90 for @ interpretation "Substitution for Formula" 'substitution b a t = (subst b a t). definition equiv ≝ λF1,F2. ∀v.[[ F1 ]]v = [[ F2 ]]v. notation "hvbox(a \nbsp break mstyle color #0000ff (≡) \nbsp b)" non associative with precedence 45 for @{ 'equivF $a $b }. -notation > "a ≡ b" non associative with precedence 50 for @{ equiv $a $b }. +notation > "a ≡ b" non associative with precedence 55 for @{ equiv $a $b }. interpretation "equivalence for Formulas" 'equivF a b = (equiv a b). (* Test 2 diff --git a/matita/matita/library/nat/pi_p.ma b/matita/matita/library/nat/pi_p.ma index b526e8d51..cf7969841 100644 --- a/matita/matita/library/nat/pi_p.ma +++ b/matita/matita/library/nat/pi_p.ma @@ -29,28 +29,28 @@ notation < "(mstyle scriptlevel 1 scriptsizemultiplier 1.7(Π) ­ (p \atop (ident i < n)) f" -non associative with precedence 60 for +non associative with precedence 65 for @{ 'product $n (λ${ident i}:$xx1.$p) (λ${ident i}:$xx2.$f) }. notation < "(mstyle scriptlevel 1 scriptsizemultiplier 1.7(Π) ­ ) \below ((ident i < n)) f" -non associative with precedence 60 for +non associative with precedence 65 for @{ 'product $n (λ_:$xx1.$xx3) (λ${ident i}:$xx2.$f) }. interpretation "big product" 'product n p f = (pi_p n p f). notation > "'Pi' (ident x) < n | p . term 46 f" -non associative with precedence 60 +non associative with precedence 65 for @{ 'product $n (λ${ident x}.$p) (λ${ident x}.$f) }. notation > "'Pi' (ident x) ≤ n | p . term 46 f" -non associative with precedence 60 +non associative with precedence 65 for @{ 'product (S $n) (λ${ident x}.$p) (λ${ident x}.$f) }. notation > "'Pi' (ident x) < n . term 46 f" -non associative with precedence 60 +non associative with precedence 65 for @{ 'product $n (λ_.true) (λ${ident x}.$f) }. *) diff --git a/matita/matita/nlibrary/PTS/gpts.ma b/matita/matita/nlibrary/PTS/gpts.ma index 9af902252..d866087a8 100644 --- a/matita/matita/nlibrary/PTS/gpts.ma +++ b/matita/matita/nlibrary/PTS/gpts.ma @@ -52,7 +52,7 @@ ninductive TJ: list T → T → T → Prop ≝ | conv: ∀G.∀A,B,C.∀i. conv B C → TJ G A B → TJ G B (Sort i) → TJ G A C. -notation "hvbox(G break ⊢ A : B)" non associative with precedence 50 for @{'TJ $G $A $B}. +notation "hvbox(G break ⊢ A : B)" non associative with precedence 55 for @{'TJ $G $A $B}. interpretation "type judgement" 'TJ G A B = (TJ G A B). (* ninverter TJ_inv2 for TJ (%?%) : Prop. *) diff --git a/matita/matita/nlibrary/basics/list2.ma b/matita/matita/nlibrary/basics/list2.ma index 1dd62c114..094738c03 100644 --- a/matita/matita/nlibrary/basics/list2.ma +++ b/matita/matita/nlibrary/basics/list2.ma @@ -20,7 +20,7 @@ nlet rec length (A:Type) (l:list A) on l ≝ [ nil ⇒ 0 | cons a tl ⇒ S (length A tl)]. -notation "|M|" non associative with precedence 60 for @{'norm $M}. +notation "|M|" non associative with precedence 65 for @{'norm $M}. interpretation "norm" 'norm l = (length ? l). nlet rec nth n (A:Type) (l:list A) (d:A) ≝ diff --git a/matita/matita/nlibrary/core_notation.ma b/matita/matita/nlibrary/core_notation.ma index 9cc0cca3c..0931115db 100644 --- a/matita/matita/nlibrary/core_notation.ma +++ b/matita/matita/nlibrary/core_notation.ma @@ -144,23 +144,23 @@ notation "hvbox(a break \ndivides b)" for @{ 'ndivides $a $b }. notation "hvbox(a break + b)" - left associative with precedence 50 + left associative with precedence 55 for @{ 'plus $a $b }. notation "hvbox(a break - b)" - left associative with precedence 50 + left associative with precedence 55 for @{ 'minus $a $b }. notation "hvbox(a break * b)" - left associative with precedence 55 + left associative with precedence 60 for @{ 'times $a $b }. notation "hvbox(a break \middot b)" - left associative with precedence 55 + left associative with precedence 60 for @{ 'middot $a $b }. notation "hvbox(a break \mod b)" - left associative with precedence 55 + left associative with precedence 60 for @{ 'module $a $b }. notation < "a \frac b" @@ -168,14 +168,14 @@ notation < "a \frac b" for @{ 'divide $a $b }. notation "a \over b" - left associative with precedence 55 + left associative with precedence 60 for @{ 'divide $a $b }. notation "hvbox(a break / b)" - left associative with precedence 55 + left associative with precedence 60 for @{ 'divide $a $b }. -notation "- term 60 a" with precedence 60 +notation "- term 65 a" with precedence 65 for @{ 'uminus $a }. notation "a !" @@ -183,7 +183,7 @@ notation "a !" for @{ 'fact $a }. notation "\sqrt a" - non associative with precedence 60 + non associative with precedence 65 for @{ 'sqrt $a }. notation "hvbox(a break \lor b)" @@ -233,10 +233,10 @@ for @{ 'overlaps $a $b }. (* \between *) notation "hvbox(a break ⊆ b)" non associative with precedence 45 for @{ 'subseteq $a $b }. (* \subseteq *) -notation "hvbox(a break ∩ b)" left associative with precedence 55 +notation "hvbox(a break ∩ b)" left associative with precedence 60 for @{ 'intersects $a $b }. (* \cap *) -notation "hvbox(a break ∪ b)" left associative with precedence 50 +notation "hvbox(a break ∪ b)" left associative with precedence 55 for @{ 'union $a $b }. (* \cup *) notation "hvbox({ term 19 a })" with precedence 90 for @{ 'singl $a}. @@ -248,17 +248,17 @@ notation "hvbox(a break # b)" non associative with precedence 45 for @{ 'apart $a $b}. notation "hvbox(a break \circ b)" - left associative with precedence 55 + left associative with precedence 60 for @{ 'compose $a $b }. -notation < "↓ \ensp a" with precedence 55 for @{ 'downarrow $a }. -notation > "↓ a" with precedence 55 for @{ 'downarrow $a }. +notation < "↓ \ensp a" with precedence 60 for @{ 'downarrow $a }. +notation > "↓ a" with precedence 60 for @{ 'downarrow $a }. -notation "hvbox(U break ↓ V)" non associative with precedence 55 for @{ 'fintersects $U $V }. +notation "hvbox(U break ↓ V)" non associative with precedence 60 for @{ 'fintersects $U $V }. -notation "↑a" with precedence 55 for @{ 'uparrow $a }. +notation "↑a" with precedence 60 for @{ 'uparrow $a }. -notation "hvbox(a break ↑ b)" with precedence 55 for @{ 'funion $a $b }. +notation "hvbox(a break ↑ b)" with precedence 60 for @{ 'funion $a $b }. notation < "term 76 a \sup term 90 b" non associative with precedence 75 for @{ 'exp $a $b}. notation > "a \sup term 90 b" non associative with precedence 75 for @{ 'exp $a $b}. @@ -280,8 +280,8 @@ notation "\ee" with precedence 90 for @{ 'neutral }. (* ⅇ *) notation > "x ⊩ y" with precedence 45 for @{'Vdash2 $x $y ?}. notation > "x ⊩⎽ term 90 c y" with precedence 45 for @{'Vdash2 $x $y $c}. notation "x (⊩ \sub term 90 c) y" with precedence 45 for @{'Vdash2 $x $y $c}. -notation > "⊩ " with precedence 60 for @{'Vdash ?}. -notation "(⊩ \sub term 90 c) " with precedence 60 for @{'Vdash $c}. +notation > "⊩ " with precedence 65 for @{'Vdash ?}. +notation "(⊩ \sub term 90 c) " with precedence 65 for @{'Vdash $c}. notation < "maction (mstyle color #ff0000 (­…­)) (t)" non associative with precedence 90 for @{'hide $t}. diff --git a/matita/matita/nlibrary/logic/cprop.ma b/matita/matita/nlibrary/logic/cprop.ma index e7ecf01ad..2c5303c56 100644 --- a/matita/matita/nlibrary/logic/cprop.ma +++ b/matita/matita/nlibrary/logic/cprop.ma @@ -39,7 +39,7 @@ ndefinition fi': ∀A,B:CPROP. A = B → B → A. #A; #B; #H; napply (fi … H); nassumption. nqed. -notation ". r" with precedence 50 for @{'fi $r}. +notation ". r" with precedence 55 for @{'fi $r}. interpretation "fi" 'fi r = (fi' ?? r). ndefinition and_morphism: unary_morphism1 CPROP (unary_morphism1_setoid1 CPROP CPROP). @@ -227,7 +227,7 @@ nqed. - x1...xn are bound in E and P, H is bound in P - H is an identifier that will have the type of E in P - P is the proof that the two existentially quantified predicates are equal*) -notation > "∑ list1 ident x sep , . term 56 E / ident nE ; term 19 H" with precedence 20 +notation > "∑ list1 ident x sep , . term 61 E / ident nE ; term 19 H" with precedence 20 for @{ 'Sig_gen ${ fold right @{ 'End } rec acc @{ ('Next (λ${ident x}.${ident x}) $acc) } } ${ fold right @{ $E } rec acc @{ λ${ident x}.$acc } } @@ -262,4 +262,4 @@ nlemma test3 : ∀S:setoid. ∀ee: (setoid1_of_setoid S) ⇒_1 (setoid1_of_setoi ((Ex S (λw.ee x w ∧ True) ∨ True)) =_1 ((Ex S (λw.ee y w ∧ True) ∨ True)). #S m x y E; napply (.=_1 (∑w. E / E ; ((E ╪_1 #) ╪_1 #)) ╪_1 #). //; nqed. *) - \ No newline at end of file + diff --git a/matita/matita/nlibrary/overlap/o-algebra.ma b/matita/matita/nlibrary/overlap/o-algebra.ma index 40b2f72bb..e4dcec628 100644 --- a/matita/matita/nlibrary/overlap/o-algebra.ma +++ b/matita/matita/nlibrary/overlap/o-algebra.ma @@ -70,11 +70,11 @@ for @{ 'overlap $a $b}. interpretation "o-algebra overlap" 'overlap a b = (fun11 ?? (fun11 ?? (oa_overlap ?) a) b). notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∧) \below (\emsp) \nbsp term 90 p)" -non associative with precedence 50 for @{ 'oa_meet $p }. +non associative with precedence 55 for @{ 'oa_meet $p }. notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∧) \below (ident i ∈  I) break term 90 p)" -non associative with precedence 50 for @{ 'oa_meet_mk (λ${ident i}:$I.$p) }. +non associative with precedence 55 for @{ 'oa_meet_mk (λ${ident i}:$I.$p) }. -(*notation > "hovbox(∧ f)" non associative with precedence 60 +(*notation > "hovbox(∧ f)" non associative with precedence 65 for @{ 'oa_meet $f }. interpretation "o-algebra meet" 'oa_meet f = (fun12 ?? (oa_meet ??) f). @@ -82,12 +82,12 @@ interpretation "o-algebra meet with explicit function" 'oa_meet_mk f = (fun12 ?? (oa_meet ??) (mk_unary_morphism ?? f ?)). *) notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∨) \below (\emsp) \nbsp term 90 p)" -non associative with precedence 50 for @{ 'oa_join $p }. +non associative with precedence 55 for @{ 'oa_join $p }. notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∨) \below (ident i ∈  I) break term 90 p)" -non associative with precedence 50 for @{ 'oa_join_mk (λ${ident i}:$I.$p) }. +non associative with precedence 55 for @{ 'oa_join_mk (λ${ident i}:$I.$p) }. (*CSC -notation > "hovbox(∨ f)" non associative with precedence 60 +notation > "hovbox(∨ f)" non associative with precedence 65 for @{ 'oa_join $f }. interpretation "o-algebra join" 'oa_join f = (fun12 ?? (oa_join ??) f). @@ -141,7 +141,7 @@ non associative with precedence 49 for @{ 'oa_join_mk (λ${ident i}:$I.$p) }. notation < "hovbox(a ∨ b)" left associative with precedence 49 for @{ 'oa_join_mk (λ${ident i}:$_.match $i with [ true ⇒ $a | false ⇒ $b ]) }. -notation > "hovbox(∨ f)" non associative with precedence 59 +notation > "hovbox(∨ f)" non associative with precedence 64 for @{ 'oa_join $f }. notation > "hovbox(a ∨ b)" left associative with precedence 49 for @{ 'oa_join (mk_unary_morphism BOOL ? (λx__:bool.match x__ with [ true ⇒ $a | false ⇒ $b ]) (IF_THEN_ELSE_p ? $a $b)) }. diff --git a/matita/matita/nlibrary/re/re-setoids.ma b/matita/matita/nlibrary/re/re-setoids.ma index 70b39c7c4..79f6b49d9 100644 --- a/matita/matita/nlibrary/re/re-setoids.ma +++ b/matita/matita/nlibrary/re/re-setoids.ma @@ -97,7 +97,7 @@ notation > "a ^ *" non associative with precedence 75 for @{ 'pk $a}. interpretation "star" 'pk a = (k ? a). interpretation "or" 'plus a b = (o ? a b). -notation "a · b" non associative with precedence 60 for @{ 'pc $a $b}. +notation "a · b" non associative with precedence 65 for @{ 'pc $a $b}. interpretation "cat" 'pc a b = (c ? a b). (* to get rid of \middot *) @@ -629,7 +629,7 @@ nlemma not_epsilon_lp : ∀S:Alpha.∀e:pitem S. ¬ ([ ] ∈ (𝐋\p e)). nqed. ndefinition lo ≝ λS:Alpha.λa,b:pre S.〈\fst a + \fst b,\snd a || \snd b〉. -notation "a ⊕ b" left associative with precedence 60 for @{'oplus $a $b}. +notation "a ⊕ b" left associative with precedence 65 for @{'oplus $a $b}. interpretation "oplus" 'oplus a b = (lo ? a b). ndefinition lc ≝ λS:Alpha.λbcast:∀S:Alpha.∀E:pitem S.pre S.λa,b:pre S. @@ -638,9 +638,9 @@ ndefinition lc ≝ λS:Alpha.λbcast:∀S:Alpha.∀E:pitem S.pre S.λa,b:pre S. [ false ⇒ 〈e1 · \fst b, \snd b〉 | true ⇒ 〈e1 · \fst (bcast ? (\fst b)),\snd b || \snd (bcast ? (\fst b))〉]]. -notation < "a ⊙ b" left associative with precedence 60 for @{'lc $op $a $b}. +notation < "a ⊙ b" left associative with precedence 65 for @{'lc $op $a $b}. interpretation "lc" 'lc op a b = (lc ? op a b). -notation > "a ⊙ b" left associative with precedence 60 for @{'lc eclose $a $b}. +notation > "a ⊙ b" left associative with precedence 65 for @{'lc eclose $a $b}. ndefinition lk ≝ λS:Alpha.λbcast:∀S:Alpha.∀E:pitem S.pre S.λa:pre S. match a with [ mk_pair e1 b1 ⇒ @@ -652,7 +652,7 @@ notation < "a \sup ⊛" non associative with precedence 90 for @{'lk $op $a}. interpretation "lk" 'lk op a = (lk ? op a). notation > "a ^ ⊛" non associative with precedence 75 for @{'lk eclose $a}. -notation > "•" non associative with precedence 60 for @{eclose ?}. +notation > "•" non associative with precedence 65 for @{eclose ?}. nlet rec eclose (S: Alpha) (E: pitem S) on E : pre S ≝ match E with [ pz ⇒ 〈 0, false 〉 @@ -662,9 +662,9 @@ nlet rec eclose (S: Alpha) (E: pitem S) on E : pre S ≝ | po E1 E2 ⇒ •E1 ⊕ •E2 | pc E1 E2 ⇒ •E1 ⊙ 〈 E2, false 〉 | pk E ⇒ 〈(\fst (•E))^*,true〉]. -notation < "• x" non associative with precedence 60 for @{'eclose $x}. +notation < "• x" non associative with precedence 65 for @{'eclose $x}. interpretation "eclose" 'eclose x = (eclose ? x). -notation > "• x" non associative with precedence 60 for @{'eclose $x}. +notation > "• x" non associative with precedence 65 for @{'eclose $x}. ndefinition reclose ≝ λS:Alpha.λp:pre S.let p' ≝ •\fst p in 〈\fst p',\snd p || \snd p'〉. interpretation "reclose" 'eclose x = (reclose ? x). @@ -983,7 +983,7 @@ ntheorem bull_true_epsilon : ∀S.∀e:pitem S. \snd (•e) = true ↔ [ ] ∈ . STOP notation > "\move term 90 x term 90 E" -non associative with precedence 60 for @{move ? $x $E}. +non associative with precedence 65 for @{move ? $x $E}. nlet rec move (S: Alpha) (x:S) (E: pitem S) on E : pre S ≝ match E with [ pz ⇒ 〈 ∅, false 〉 @@ -993,8 +993,8 @@ nlet rec move (S: Alpha) (x:S) (E: pitem S) on E : pre S ≝ | po e1 e2 ⇒ \move x e1 ⊕ \move x e2 | pc e1 e2 ⇒ \move x e1 ⊙ \move x e2 | pk e ⇒ (\move x e)^⊛ ]. -notation < "\move\shy x\shy E" non associative with precedence 60 for @{'move $x $E}. -notation > "\move term 90 x term 90 E" non associative with precedence 60 for @{'move $x $E}. +notation < "\move\shy x\shy E" non associative with precedence 65 for @{'move $x $E}. +notation > "\move term 90 x term 90 E" non associative with precedence 65 for @{'move $x $E}. interpretation "move" 'move x E = (move ? x E). ndefinition rmove ≝ λS:Alpha.λx:S.λe:pre S. \move x (\fst e). @@ -1064,7 +1064,7 @@ ntheorem move_ok: nqed. -notation > "x ↦* E" non associative with precedence 60 for @{move_star ? $x $E}. +notation > "x ↦* E" non associative with precedence 65 for @{move_star ? $x $E}. nlet rec move_star (S : decidable) w E on w : bool × (pre S) ≝ match w with [ nil ⇒ E diff --git a/matita/matita/nlibrary/re/re.ma b/matita/matita/nlibrary/re/re.ma index 40947401f..d0690ca26 100644 --- a/matita/matita/nlibrary/re/re.ma +++ b/matita/matita/nlibrary/re/re.ma @@ -41,7 +41,7 @@ notation > "a ^ *" non associative with precedence 90 for @{ 'pk $a}. interpretation "star" 'pk a = (k ? a). interpretation "or" 'plus a b = (o ? a b). -notation "a · b" non associative with precedence 60 for @{ 'pc $a $b}. +notation "a · b" non associative with precedence 65 for @{ 'pc $a $b}. interpretation "cat" 'pc a b = (c ? a b). (* to get rid of \middot *) @@ -193,7 +193,7 @@ nlemma not_epsilon_lp : ∀S:Alpha.∀e:pitem S. ¬ ((𝐋\p e) [ ]). nqed. ndefinition lo ≝ λS:Alpha.λa,b:pre S.〈\fst a + \fst b,\snd a || \snd b〉. -notation "a ⊕ b" left associative with precedence 60 for @{'oplus $a $b}. +notation "a ⊕ b" left associative with precedence 65 for @{'oplus $a $b}. interpretation "oplus" 'oplus a b = (lo ? a b). ndefinition lc ≝ λS:Alpha.λbcast:∀S:Alpha.∀E:pitem S.pre S.λa,b:pre S. @@ -202,9 +202,9 @@ ndefinition lc ≝ λS:Alpha.λbcast:∀S:Alpha.∀E:pitem S.pre S.λa,b:pre S. [ false ⇒ 〈e1 · \fst b, \snd b〉 | true ⇒ 〈e1 · \fst (bcast ? (\fst b)),\snd b || \snd (bcast ? (\fst b))〉]]. -notation < "a ⊙ b" left associative with precedence 60 for @{'lc $op $a $b}. +notation < "a ⊙ b" left associative with precedence 65 for @{'lc $op $a $b}. interpretation "lc" 'lc op a b = (lc ? op a b). -notation > "a ⊙ b" left associative with precedence 60 for @{'lc eclose $a $b}. +notation > "a ⊙ b" left associative with precedence 65 for @{'lc eclose $a $b}. ndefinition lk ≝ λS:Alpha.λbcast:∀S:Alpha.∀E:pitem S.pre S.λa:pre S. match a with [ mk_pair e1 b1 ⇒ @@ -216,7 +216,7 @@ notation < "a \sup ⊛" non associative with precedence 90 for @{'lk $op $a}. interpretation "lk" 'lk op a = (lk ? op a). notation > "a^⊛" non associative with precedence 90 for @{'lk eclose $a}. -notation > "•" non associative with precedence 60 for @{eclose ?}. +notation > "•" non associative with precedence 65 for @{eclose ?}. nlet rec eclose (S: Alpha) (E: pitem S) on E : pre S ≝ match E with [ pz ⇒ 〈 ∅, false 〉 @@ -226,9 +226,9 @@ nlet rec eclose (S: Alpha) (E: pitem S) on E : pre S ≝ | po E1 E2 ⇒ •E1 ⊕ •E2 | pc E1 E2 ⇒ •E1 ⊙ 〈 E2, false 〉 | pk E ⇒ 〈(\fst (•E))^*,true〉]. -notation < "• x" non associative with precedence 60 for @{'eclose $x}. +notation < "• x" non associative with precedence 65 for @{'eclose $x}. interpretation "eclose" 'eclose x = (eclose ? x). -notation > "• x" non associative with precedence 60 for @{'eclose $x}. +notation > "• x" non associative with precedence 65 for @{'eclose $x}. ndefinition reclose ≝ λS:Alpha.λp:pre S.let p' ≝ •\fst p in 〈\fst p',\snd p || \snd p'〉. interpretation "reclose" 'eclose x = (reclose ? x). @@ -525,7 +525,7 @@ ntheorem bull_true_epsilon : ∀S.∀e:pitem S. \snd (•e) = true ↔ [ ] ∈ | STOP notation > "\move term 90 x term 90 E" -non associative with precedence 60 for @{move ? $x $E}. +non associative with precedence 65 for @{move ? $x $E}. nlet rec move (S: Alpha) (x:S) (E: pitem S) on E : pre S ≝ match E with [ pz ⇒ 〈 ∅, false 〉 @@ -535,8 +535,8 @@ nlet rec move (S: Alpha) (x:S) (E: pitem S) on E : pre S ≝ | po e1 e2 ⇒ \move x e1 ⊕ \move x e2 | pc e1 e2 ⇒ \move x e1 ⊙ \move x e2 | pk e ⇒ (\move x e)^⊛ ]. -notation < "\move\shy x\shy E" non associative with precedence 60 for @{'move $x $E}. -notation > "\move term 90 x term 90 E" non associative with precedence 60 for @{'move $x $E}. +notation < "\move\shy x\shy E" non associative with precedence 65 for @{'move $x $E}. +notation > "\move term 90 x term 90 E" non associative with precedence 65 for @{'move $x $E}. interpretation "move" 'move x E = (move ? x E). ndefinition rmove ≝ λS:Alpha.λx:S.λe:pre S. \move x (\fst e). @@ -606,7 +606,7 @@ ntheorem move_ok: nqed. -notation > "x ↦* E" non associative with precedence 60 for @{move_star ? $x $E}. +notation > "x ↦* E" non associative with precedence 65 for @{move_star ? $x $E}. nlet rec move_star (S : decidable) w E on w : bool × (pre S) ≝ match w with [ nil ⇒ E diff --git a/matita/matita/nlibrary/sets/categories2.ma b/matita/matita/nlibrary/sets/categories2.ma index 17d621431..8651d1854 100644 --- a/matita/matita/nlibrary/sets/categories2.ma +++ b/matita/matita/nlibrary/sets/categories2.ma @@ -32,7 +32,7 @@ nrecord category : Type[2] ≝ }. *) -notation "hvbox(A break ⇒ B)" right associative with precedence 50 for @{ 'arrows $A $B }. +notation "hvbox(A break ⇒ B)" right associative with precedence 55 for @{ 'arrows $A $B }. interpretation "arrows1" 'arrows A B = (unary_morphism1 A B). interpretation "arrows" 'arrows A B = (unary_morphism A B). diff --git a/matita/matita/nlibrary/sets/setoids.ma b/matita/matita/nlibrary/sets/setoids.ma index e40dad6f6..f54836074 100644 --- a/matita/matita/nlibrary/sets/setoids.ma +++ b/matita/matita/nlibrary/sets/setoids.ma @@ -41,9 +41,9 @@ notation > "hvbox(a break =_0 b)" non associative with precedence 45 for @{ eq_rel ? (eq0 ?) $a $b }. interpretation "setoid symmetry" 'invert r = (sym ???? r). -notation ".= r" with precedence 50 for @{'trans $r}. +notation ".= r" with precedence 55 for @{'trans $r}. interpretation "trans" 'trans r = (trans ????? r). -notation > ".=_0 r" with precedence 50 for @{'trans_x0 $r}. +notation > ".=_0 r" with precedence 55 for @{'trans_x0 $r}. interpretation "trans_x0" 'trans_x0 r = (trans ????? r). nrecord unary_morphism (A,B: setoid) : Type[0] ≝ { diff --git a/matita/matita/nlibrary/sets/setoids1.ma b/matita/matita/nlibrary/sets/setoids1.ma index 90be6bc94..74d7d9e8e 100644 --- a/matita/matita/nlibrary/sets/setoids1.ma +++ b/matita/matita/nlibrary/sets/setoids1.ma @@ -61,7 +61,7 @@ for @{ eq_rel1 ? (eq1 ?) $a $b }. interpretation "setoid1 symmetry" 'invert r = (sym1 ???? r). interpretation "setoid symmetry" 'invert r = (sym ???? r). -notation ".=_1 r" with precedence 50 for @{'trans_x1 $r}. +notation ".=_1 r" with precedence 55 for @{'trans_x1 $r}. interpretation "trans1" 'trans r = (trans1 ????? r). interpretation "trans" 'trans r = (trans ????? r). interpretation "trans1_x1" 'trans_x1 r = (trans1 ????? r). diff --git a/matita/matita/nlibrary/sets/setoids2.ma b/matita/matita/nlibrary/sets/setoids2.ma index 34036a48b..ba2c1c52b 100644 --- a/matita/matita/nlibrary/sets/setoids2.ma +++ b/matita/matita/nlibrary/sets/setoids2.ma @@ -49,7 +49,7 @@ for @{ eq_rel2 ? (eq2 ?) $a $b }. interpretation "setoid2 symmetry" 'invert r = (sym2 ???? r). interpretation "setoid1 symmetry" 'invert r = (sym1 ???? r). interpretation "setoid symmetry" 'invert r = (sym ???? r). -notation ".= r" with precedence 50 for @{'trans $r}. +notation ".= r" with precedence 55 for @{'trans $r}. interpretation "trans2" 'trans r = (trans2 ????? r). interpretation "trans1" 'trans r = (trans1 ????? r). interpretation "trans" 'trans r = (trans ????? r). diff --git a/matita/matita/nlibrary/topology/igft-setoid.ma b/matita/matita/nlibrary/topology/igft-setoid.ma index a4d833cae..15c3320f2 100644 --- a/matita/matita/nlibrary/topology/igft-setoid.ma +++ b/matita/matita/nlibrary/topology/igft-setoid.ma @@ -25,7 +25,7 @@ nrecord category : Type[2] ≝ id_neutral_right: ∀o1,o2. ∀a: arrows o1 o2. comp ??? a (id o2) = a }. -notation "hvbox(A break ⇒ B)" right associative with precedence 50 for @{ 'arrows $A $B }. +notation "hvbox(A break ⇒ B)" right associative with precedence 55 for @{ 'arrows $A $B }. interpretation "arrows" 'arrows A B = (unary_morphism A B). notation > "𝐈𝐝 term 90 A" non associative with precedence 90 for @{ 'id $A }. @@ -162,8 +162,8 @@ ninductive Ord (A : nAx) : Type[0] ≝ | oL : ∀a:A.∀i.∀f:𝐃 a i → Ord A. Ord A. notation "0" non associative with precedence 90 for @{ 'oO }. -notation "Λ term 90 f" non associative with precedence 50 for @{ 'oL $f }. -notation "x+1" non associative with precedence 50 for @{'oS $x }. +notation "Λ term 90 f" non associative with precedence 55 for @{ 'oL $f }. +notation "x+1" non associative with precedence 55 for @{'oS $x }. interpretation "ordinals Zero" 'oO = (oO ?). interpretation "ordinals Lambda" 'oL f = (oL ? ? ? f). @@ -194,8 +194,8 @@ nlet rec famU (A : nAx) (U : 𝛀^A) (x : Ord A) on x : 𝛀^A ≝ (* -notation < "term 90 U \sub (term 90 x)" non associative with precedence 50 for @{ 'famU $U $x }. -notation > "U ⎽ term 90 x" non associative with precedence 50 for @{ 'famU $U $x }. +notation < "term 90 U \sub (term 90 x)" non associative with precedence 55 for @{ 'famU $U $x }. +notation > "U ⎽ term 90 x" non associative with precedence 55 for @{ 'famU $U $x }. interpretation "famU" 'famU U x = (famU ? U x). diff --git a/matita/matita/nlibrary/topology/igft.ma b/matita/matita/nlibrary/topology/igft.ma index d6043fba2..aa2d6704b 100644 --- a/matita/matita/nlibrary/topology/igft.ma +++ b/matita/matita/nlibrary/topology/igft.ma @@ -781,7 +781,7 @@ D*) ndefinition coverage : ∀A:Ax.∀U:Ω^A.Ω^A ≝ λA,U.{ a | a ◃ U }. -notation "◃U" non associative with precedence 55 for @{ 'coverage $U }. +notation "◃U" non associative with precedence 60 for @{ 'coverage $U }. interpretation "coverage cover" 'coverage U = (coverage ? U). @@ -826,7 +826,7 @@ the biggest solution for such equation. D*) -notation "⋉F" non associative with precedence 55 +notation "⋉F" non associative with precedence 60 for @{ 'fished $F }. ndefinition fished : ∀A:Ax.∀F:Ω^A.Ω^A ≝ λA,F.{ a | a ⋉ F }. @@ -1039,8 +1039,8 @@ ninductive Ord (A : nAx) : Type[0] ≝ | oL : ∀a:A.∀i.∀f:𝐃 a i → Ord A. Ord A. notation "0" non associative with precedence 90 for @{ 'oO }. -notation "x+1" non associative with precedence 50 for @{'oS $x }. -notation "Λ term 90 f" non associative with precedence 50 for @{ 'oL $f }. +notation "x+1" non associative with precedence 55 for @{'oS $x }. +notation "Λ term 90 f" non associative with precedence 55 for @{ 'oL $f }. interpretation "ordinals Zero" 'oO = (oO ?). interpretation "ordinals Succ" 'oS x = (oS ? x). @@ -1068,8 +1068,8 @@ nlet rec famU (A : nAx) (U : Ω^A) (x : Ord A) on x : Ω^A ≝ | oS y ⇒ let U_n ≝ famU A U y in U_n ∪ { x | ∃i.𝐈𝐦[𝐝 x i] ⊆ U_n} | oL a i f ⇒ { x | ∃j.x ∈ famU A U (f j) } ]. -notation < "term 90 U \sub (term 90 x)" non associative with precedence 50 for @{ 'famU $U $x }. -notation > "U ⎽ term 90 x" non associative with precedence 50 for @{ 'famU $U $x }. +notation < "term 90 U \sub (term 90 x)" non associative with precedence 55 for @{ 'famU $U $x }. +notation > "U ⎽ term 90 x" non associative with precedence 55 for @{ 'famU $U $x }. interpretation "famU" 'famU U x = (famU ? U x). diff --git a/matita/matita/re_complete/basics/core_notation.ma b/matita/matita/re_complete/basics/core_notation.ma index 4eae6c6c3..904adcd52 100644 --- a/matita/matita/re_complete/basics/core_notation.ma +++ b/matita/matita/re_complete/basics/core_notation.ma @@ -175,23 +175,23 @@ notation "hvbox(a break \ndivides b)" for @{ 'ndivides $a $b }. notation "hvbox(a break + b)" - left associative with precedence 50 + left associative with precedence 55 for @{ 'plus $a $b }. notation "hvbox(a break - b)" - left associative with precedence 50 + left associative with precedence 55 for @{ 'minus $a $b }. notation "hvbox(a break * b)" - left associative with precedence 55 + left associative with precedence 60 for @{ 'times $a $b }. notation "hvbox(a break \middot b)" - left associative with precedence 55 + left associative with precedence 60 for @{ 'middot $a $b }. notation "hvbox(a break \mod b)" - left associative with precedence 55 + left associative with precedence 60 for @{ 'module $a $b }. notation < "a \frac b" @@ -199,14 +199,14 @@ notation < "a \frac b" for @{ 'divide $a $b }. notation "a \over b" - left associative with precedence 55 + left associative with precedence 60 for @{ 'divide $a $b }. notation "hvbox(a break / b)" - left associative with precedence 55 + left associative with precedence 60 for @{ 'divide $a $b }. -notation "- term 60 a" with precedence 60 +notation "- term 65 a" with precedence 65 for @{ 'uminus $a }. notation "a !" @@ -214,7 +214,7 @@ notation "a !" for @{ 'fact $a }. notation "\sqrt a" - non associative with precedence 60 + non associative with precedence 65 for @{ 'sqrt $a }. notation "hvbox(a break \lor b)" @@ -264,10 +264,10 @@ for @{ 'overlaps $a $b }. (* \between *) notation "hvbox(a break ⊆ b)" non associative with precedence 45 for @{ 'subseteq $a $b }. (* \subseteq *) -notation "hvbox(a break ∩ b)" left associative with precedence 55 +notation "hvbox(a break ∩ b)" left associative with precedence 60 for @{ 'intersects $a $b }. (* \cap *) -notation "hvbox(a break ∪ b)" left associative with precedence 50 +notation "hvbox(a break ∪ b)" left associative with precedence 55 for @{ 'union $a $b }. (* \cup *) notation "hvbox({ term 19 a })" with precedence 90 for @{ 'singl $a}. @@ -279,17 +279,17 @@ notation "hvbox(a break # b)" non associative with precedence 45 for @{ 'apart $a $b}. notation "hvbox(a break \circ b)" - left associative with precedence 55 + left associative with precedence 60 for @{ 'compose $a $b }. -notation < "↓ \ensp a" with precedence 55 for @{ 'downarrow $a }. -notation > "↓ a" with precedence 55 for @{ 'downarrow $a }. +notation < "↓ \ensp a" with precedence 60 for @{ 'downarrow $a }. +notation > "↓ a" with precedence 60 for @{ 'downarrow $a }. -notation "hvbox(U break ↓ V)" non associative with precedence 55 for @{ 'fintersects $U $V }. +notation "hvbox(U break ↓ V)" non associative with precedence 60 for @{ 'fintersects $U $V }. -notation "↑a" with precedence 55 for @{ 'uparrow $a }. +notation "↑a" with precedence 60 for @{ 'uparrow $a }. -notation "hvbox(a break ↑ b)" with precedence 55 for @{ 'funion $a $b }. +notation "hvbox(a break ↑ b)" with precedence 60 for @{ 'funion $a $b }. notation < "term 76 a \sup term 90 b" non associative with precedence 75 for @{ 'exp $a $b}. notation > "a \sup term 90 b" non associative with precedence 75 for @{ 'exp $a $b}. @@ -311,8 +311,8 @@ notation "\ee" with precedence 90 for @{ 'neutral }. (* ⅇ *) notation > "x ⊩ y" with precedence 45 for @{'Vdash2 $x $y ?}. notation > "x ⊩⎽ term 90 c y" with precedence 45 for @{'Vdash2 $x $y $c}. notation "x (⊩ \sub term 90 c) y" with precedence 45 for @{'Vdash2 $x $y $c}. -notation > "⊩ " with precedence 60 for @{'Vdash ?}. -notation "(⊩ \sub term 90 c) " with precedence 60 for @{'Vdash $c}. +notation > "⊩ " with precedence 65 for @{'Vdash ?}. +notation "(⊩ \sub term 90 c) " with precedence 65 for @{'Vdash $c}. notation < "maction (mstyle color #ff0000 (­…­)) (t)" non associative with precedence 90 for @{'hide $t}. diff --git a/matita/matita/re_complete/basics/list.ma b/matita/matita/re_complete/basics/list.ma index b0a683135..df0fa840c 100644 --- a/matita/matita/re_complete/basics/list.ma +++ b/matita/matita/re_complete/basics/list.ma @@ -151,7 +151,7 @@ let rec length (A:Type[0]) (l:list A) on l ≝ [ nil ⇒ O | cons a tl ⇒ S (length A tl)]. -notation "|M|" non associative with precedence 60 for @{'norm $M}. +notation "|M|" non associative with precedence 65 for @{'norm $M}. interpretation "norm" 'norm l = (length ? l). lemma length_append: ∀A.∀l1,l2:list A. diff --git a/matita/matita/re_complete/lang.ma b/matita/matita/re_complete/lang.ma index 430fc3f21..510d2215c 100644 --- a/matita/matita/re_complete/lang.ma +++ b/matita/matita/re_complete/lang.ma @@ -10,7 +10,7 @@ interpretation "epsilon" 'epsilon = (nil ?). (* concatenation *) definition cat : ∀S,l1,l2,w.Prop ≝ λS.λl1,l2.λw:word S.∃w1,w2.w1 @ w2 = w ∧ l1 w1 ∧ l2 w2. -notation "a · b" non associative with precedence 60 for @{ 'middot $a $b}. +notation "a · b" non associative with precedence 65 for @{ 'middot $a $b}. interpretation "cat lang" 'middot a b = (cat ? a b). let rec flatten (S : DeqSet) (l : list (word S)) on l : word S ≝ diff --git a/matita/matita/re_complete/moves.ma b/matita/matita/re_complete/moves.ma index dc7474e21..a14487498 100644 --- a/matita/matita/re_complete/moves.ma +++ b/matita/matita/re_complete/moves.ma @@ -68,7 +68,7 @@ theorem move_ok: ] qed. -notation > "x ↦* E" non associative with precedence 60 for @{moves ? $x $E}. +notation > "x ↦* E" non associative with precedence 65 for @{moves ? $x $E}. let rec moves (S : DeqSet) w e on w : pre S ≝ match w with [ nil ⇒ e diff --git a/matita/matita/re_complete/re.ma b/matita/matita/re_complete/re.ma index ff1f95993..5aff713ad 100644 --- a/matita/matita/re_complete/re.ma +++ b/matita/matita/re_complete/re.ma @@ -231,7 +231,7 @@ lemma minus_eps_pre: ∀S.∀e:pre S. \sem{\fst e} =1 \sem{e}-{[ ]}. qed. definition lo ≝ λS:DeqSet.λa,b:pre S.〈\fst a + \fst b,\snd a ∨ \snd b〉. -notation "a ⊕ b" left associative with precedence 60 for @{'oplus $a $b}. +notation "a ⊕ b" left associative with precedence 65 for @{'oplus $a $b}. interpretation "oplus" 'oplus a b = (lo ? a b). lemma lo_def: ∀S.∀i1,i2:pitem S.∀b1,b2. 〈i1,b1〉⊕〈i2,b2〉=〈i1+i2,b1∨b2〉. @@ -240,7 +240,7 @@ lemma lo_def: ∀S.∀i1,i2:pitem S.∀b1,b2. 〈i1,b1〉⊕〈i2,b2〉=〈i1+i2 definition pre_concat_r ≝ λS:DeqSet.λi:pitem S.λe:pre S. match e with [ mk_Prod i1 b ⇒ 〈i · i1, b〉]. -notation "i ◃ e" left associative with precedence 60 for @{'lhd $i $e}. +notation "i ◃ e" left associative with precedence 65 for @{'lhd $i $e}. interpretation "pre_concat_r" 'lhd i e = (pre_concat_r ? i e). lemma eq_to_ex_eq: ∀S.∀A,B:word S → Prop. @@ -261,10 +261,10 @@ definition pre_concat_l ≝ λS:DeqSet.λbcast:∀S:DeqSet.pitem S → pre S.λe ] ]. -notation "a ▹ b" left associative with precedence 60 for @{'tril eclose $a $b}. +notation "a ▹ b" left associative with precedence 65 for @{'tril eclose $a $b}. interpretation "item-pre concat" 'tril op a b = (pre_concat_l ? op a b). -notation "•" non associative with precedence 60 for @{eclose ?}. +notation "•" non associative with precedence 65 for @{eclose ?}. let rec eclose (S: DeqSet) (i: pitem S) on i : pre S ≝ match i with @@ -276,7 +276,7 @@ let rec eclose (S: DeqSet) (i: pitem S) on i : pre S ≝ | pc i1 i2 ⇒ •i1 ▹ i2 | pk i ⇒ 〈(\fst (•i))^*,true〉]. -notation "• x" non associative with precedence 60 for @{'eclose $x}. +notation "• x" non associative with precedence 65 for @{'eclose $x}. interpretation "eclose" 'eclose x = (eclose ? x). lemma eclose_plus: ∀S:DeqSet.∀i1,i2:pitem S. diff --git a/matita/matita/tests/color.ma b/matita/matita/tests/color.ma index a00c3f9ff..456974c56 100644 --- a/matita/matita/tests/color.ma +++ b/matita/matita/tests/color.ma @@ -13,7 +13,7 @@ (**************************************************************************) notation < "mstyle mathsize big color #ff0000 background #0000ff scriptsizemultiplier 0.8 (x)" - non associative with precedence 50 for @{'red $x}. + non associative with precedence 55 for @{'red $x}. definition red : ∀X:Type.∀t:X.X ≝ λT.λt.t. interpretation "red" 'red x = (red _ x). -- 2.39.2