From b5cb5cc7230870f757aadbe6b43ee146fe485a6d Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 30 Mar 2018 00:28:23 +0200 Subject: [PATCH] decentralizing core notation centralized core notation (one single file) has two disadvantages: - when some core notation is added the whole "world" must be recompiled - unused core notation loaded in the parser gets in the way when defining contrib-specific notation by defining core notation on a "one notation per file" basis: + every contrib file can load just the needed notation + sharing is possible as before in that two contrib files can load the same notation file decentralalization will occur is stages: this is the first stage meant to solve some issues in + lambdadelta (! blocked by fact) + certifiedRev (o{} blocked by compose, comprehension, singl, subset) --- matita/matita/lib/arithmetics/factorial.ma | 1 + matita/matita/lib/basics/core_notation.ma | 23 +----------------- .../lib/basics/core_notation/compose_2.ma | 16 +++++++++++++ .../basics/core_notation/comprehension_2.ma | 18 ++++++++++++++ .../matita/lib/basics/core_notation/fact_1.ma | 16 +++++++++++++ .../lib/basics/core_notation/singl_1.ma | 14 +++++++++++ .../lib/basics/core_notation/subset_1.ma | 18 ++++++++++++++ matita/matita/lib/basics/relations.ma | 1 + matita/matita/lib/basics/sets.ma | 3 ++- .../matita/lib/formal_topology/categories.ma | 3 ++- .../matita/lib/formal_topology/o-algebra.ma | 1 + .../matita/lib/formal_topology/relations.ma | 1 + matita/matita/lib/formal_topology/subsets.ma | 2 ++ matita/matita/lib/hott/Overture.ma | 1 + matita/matita/lib/hott/notations.ma | 24 ------------------- matita/matita/lib/re/reb.ma | 3 ++- matita/matita/lib/turing/wmono.ma | 1 + matita/matita/lib/tutorial/chapter6.ma | 1 + 18 files changed, 98 insertions(+), 49 deletions(-) create mode 100644 matita/matita/lib/basics/core_notation/compose_2.ma create mode 100644 matita/matita/lib/basics/core_notation/comprehension_2.ma create mode 100644 matita/matita/lib/basics/core_notation/fact_1.ma create mode 100644 matita/matita/lib/basics/core_notation/singl_1.ma create mode 100644 matita/matita/lib/basics/core_notation/subset_1.ma diff --git a/matita/matita/lib/arithmetics/factorial.ma b/matita/matita/lib/arithmetics/factorial.ma index fc2320a94..60519e982 100644 --- a/matita/matita/lib/arithmetics/factorial.ma +++ b/matita/matita/lib/arithmetics/factorial.ma @@ -10,6 +10,7 @@ V_______________________________________________________________ *) include "arithmetics/exp.ma". +include "basics/core_notation/fact_1.ma". let rec fact n ≝ match n with diff --git a/matita/matita/lib/basics/core_notation.ma b/matita/matita/lib/basics/core_notation.ma index 77e44c201..cdc535b81 100644 --- a/matita/matita/lib/basics/core_notation.ma +++ b/matita/matita/lib/basics/core_notation.ma @@ -229,10 +229,6 @@ for @{ 'divide $a $b }. notation "- term 65 a" with precedence 65 for @{ 'uminus $a }. -notation "a !" - non associative with precedence 80 -for @{ 'fact $a }. - notation "\sqrt a" non associative with precedence 65 for @{ 'sqrt $a }. @@ -263,21 +259,10 @@ for @{ 'iff $a $b }. notation "hvbox(\Omega \sup term 90 A)" non associative with precedence 90 for @{ 'powerset $A }. + notation > "hvbox(\Omega ^ term 90 A)" non associative with precedence 90 for @{ 'powerset $A }. -notation < "hvbox({ ident i | term 19 p })" with precedence 90 -for @{ 'subset (\lambda ${ident i} : $nonexistent . $p)}. - -notation > "hvbox({ ident i | term 19 p })" with precedence 90 -for @{ 'subset (\lambda ${ident i}. $p)}. - -notation < "hvbox({ ident i ∈ term 19 s | term 19 p })" with precedence 90 -for @{ 'comprehension $s (\lambda ${ident i} : $nonexistent . $p)}. - -notation > "hvbox({ ident i ∈ term 19 s | term 19 p })" with precedence 90 -for @{ 'comprehension $s (\lambda ${ident i}. $p)}. - notation "hvbox(a break ∈ b)" non associative with precedence 45 for @{ 'mem $a $b }. @@ -296,8 +281,6 @@ for @{ 'intersects $a $b }. (* \cap *) 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}. - (* other notations **********************************************************) notation "hvbox(a break \approx b)" non associative with precedence 45 @@ -305,10 +288,6 @@ notation "hvbox(a break \approx b)" non associative with precedence 45 notation "hvbox(a break # b)" non associative with precedence 45 for @{ 'apart $a $b}. - -notation "hvbox(a break \circ b)" - left associative with precedence 60 -for @{ 'compose $a $b }. notation < "↓ \ensp a" with precedence 60 for @{ 'downarrow $a }. notation > "↓ a" with precedence 60 for @{ 'downarrow $a }. diff --git a/matita/matita/lib/basics/core_notation/compose_2.ma b/matita/matita/lib/basics/core_notation/compose_2.ma new file mode 100644 index 000000000..50938de64 --- /dev/null +++ b/matita/matita/lib/basics/core_notation/compose_2.ma @@ -0,0 +1,16 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department of the University of Bologna, Italy. + ||I|| + ||T|| + ||A|| This file is distributed under the terms of the + \ / GNU General Public License Version 2 + \ / + V_______________________________________________________________ *) + +(* Core notation *******************************************************) + +notation "hvbox(a break \circ b)" + left associative with precedence 60 +for @{ 'compose $a $b }. diff --git a/matita/matita/lib/basics/core_notation/comprehension_2.ma b/matita/matita/lib/basics/core_notation/comprehension_2.ma new file mode 100644 index 000000000..c58fe4d5c --- /dev/null +++ b/matita/matita/lib/basics/core_notation/comprehension_2.ma @@ -0,0 +1,18 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department of the University of Bologna, Italy. + ||I|| + ||T|| + ||A|| This file is distributed under the terms of the + \ / GNU General Public License Version 2 + \ / + V_______________________________________________________________ *) + +(* Core notation *******************************************************) + +notation < "hvbox({ ident i ∈ term 19 s | term 19 p })" with precedence 90 +for @{ 'comprehension $s (\lambda ${ident i} : $nonexistent . $p)}. + +notation > "hvbox({ ident i ∈ term 19 s | term 19 p })" with precedence 90 +for @{ 'comprehension $s (\lambda ${ident i}. $p)}. diff --git a/matita/matita/lib/basics/core_notation/fact_1.ma b/matita/matita/lib/basics/core_notation/fact_1.ma new file mode 100644 index 000000000..7deb9a541 --- /dev/null +++ b/matita/matita/lib/basics/core_notation/fact_1.ma @@ -0,0 +1,16 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department of the University of Bologna, Italy. + ||I|| + ||T|| + ||A|| This file is distributed under the terms of the + \ / GNU General Public License Version 2 + \ / + V_______________________________________________________________ *) + +(* Core notation *******************************************************) + +notation "a !" + non associative with precedence 80 +for @{ 'fact $a }. diff --git a/matita/matita/lib/basics/core_notation/singl_1.ma b/matita/matita/lib/basics/core_notation/singl_1.ma new file mode 100644 index 000000000..95e57339a --- /dev/null +++ b/matita/matita/lib/basics/core_notation/singl_1.ma @@ -0,0 +1,14 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department of the University of Bologna, Italy. + ||I|| + ||T|| + ||A|| This file is distributed under the terms of the + \ / GNU General Public License Version 2 + \ / + V_______________________________________________________________ *) + +(* Core notation *******************************************************) + +notation "hvbox({ term 19 a })" with precedence 90 for @{ 'singl $a}. diff --git a/matita/matita/lib/basics/core_notation/subset_1.ma b/matita/matita/lib/basics/core_notation/subset_1.ma new file mode 100644 index 000000000..4fe86629a --- /dev/null +++ b/matita/matita/lib/basics/core_notation/subset_1.ma @@ -0,0 +1,18 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department of the University of Bologna, Italy. + ||I|| + ||T|| + ||A|| This file is distributed under the terms of the + \ / GNU General Public License Version 2 + \ / + V_______________________________________________________________ *) + +(* Core notation *******************************************************) + +notation < "hvbox({ ident i | term 19 p })" with precedence 90 +for @{ 'subset (\lambda ${ident i} : $nonexistent . $p)}. + +notation > "hvbox({ ident i | term 19 p })" with precedence 90 +for @{ 'subset (\lambda ${ident i}. $p)}. diff --git a/matita/matita/lib/basics/relations.ma b/matita/matita/lib/basics/relations.ma index fb0423cea..24b2c9a9e 100644 --- a/matita/matita/lib/basics/relations.ma +++ b/matita/matita/lib/basics/relations.ma @@ -10,6 +10,7 @@ V_______________________________________________________________ *) include "basics/logic.ma". +include "basics/core_notation/compose_2.ma". (********** predicates *********) diff --git a/matita/matita/lib/basics/sets.ma b/matita/matita/lib/basics/sets.ma index cdc6ac9e8..2f570c18f 100644 --- a/matita/matita/lib/basics/sets.ma +++ b/matita/matita/lib/basics/sets.ma @@ -10,6 +10,7 @@ V_______________________________________________________________ *) include "basics/logic.ma". +include "basics/core_notation/singl_1.ma". (**** a subset of A is just an object of type A→Prop ****) @@ -116,4 +117,4 @@ qed. (* substraction *) lemma substract_def:∀U.∀A,B:U→Prop. A-B ≐ A ∩ ¬B. #U #A #B #w normalize /2/ -qed. \ No newline at end of file +qed. diff --git a/matita/matita/lib/formal_topology/categories.ma b/matita/matita/lib/formal_topology/categories.ma index 5643e2f6b..02605e4a8 100644 --- a/matita/matita/lib/formal_topology/categories.ma +++ b/matita/matita/lib/formal_topology/categories.ma @@ -13,6 +13,7 @@ (**************************************************************************) include "formal_topology/cprop_connectives.ma". +include "basics/core_notation/compose_2.ma". inductive eq (A:Type[0]) (x:A) : A → CProp[0] ≝ refl: eq A x x. @@ -525,4 +526,4 @@ notation > "r⎻*" non associative with precedence 90 for @{'OR_f_minus_star $r} notation "r \sup ⎻" non associative with precedence 90 for @{'OR_f_minus $r}. notation > "r⎻" non associative with precedence 90 for @{'OR_f_minus $r}. -*) \ No newline at end of file +*) diff --git a/matita/matita/lib/formal_topology/o-algebra.ma b/matita/matita/lib/formal_topology/o-algebra.ma index 704737550..61a784605 100644 --- a/matita/matita/lib/formal_topology/o-algebra.ma +++ b/matita/matita/lib/formal_topology/o-algebra.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "basics/core_notation/comprehension_2.ma". include "formal_topology/categories.ma". (* inductive bool : Type[0] := true : bool | false : bool. diff --git a/matita/matita/lib/formal_topology/relations.ma b/matita/matita/lib/formal_topology/relations.ma index 2d5d85a6b..351699900 100644 --- a/matita/matita/lib/formal_topology/relations.ma +++ b/matita/matita/lib/formal_topology/relations.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "basics/core_notation/comprehension_2.ma". include "formal_topology/subsets.ma". (* record binary_relation (A,B: SET) : Type[1] ≝ diff --git a/matita/matita/lib/formal_topology/subsets.ma b/matita/matita/lib/formal_topology/subsets.ma index 5cb8455a0..56c2c895c 100644 --- a/matita/matita/lib/formal_topology/subsets.ma +++ b/matita/matita/lib/formal_topology/subsets.ma @@ -13,6 +13,8 @@ (**************************************************************************) include "formal_topology/categories.ma". +include "basics/core_notation/singl_1.ma". +include "basics/core_notation/subset_1.ma". (* record powerset_carrier (A: objs1 SET) : Type[1] ≝ { mem_operator: A ⇒_1 CPROP }. interpretation "powerset low" 'powerset A = (powerset_carrier A). diff --git a/matita/matita/lib/hott/Overture.ma b/matita/matita/lib/hott/Overture.ma index 3725123cc..e02683ffa 100644 --- a/matita/matita/lib/hott/Overture.ma +++ b/matita/matita/lib/hott/Overture.ma @@ -1,4 +1,5 @@ include "hott/types.ma". +include "basics/core_notation/compose_2.ma". (* * * Basic definitions of homotopy type theory, particularly the groupoid structure of identity types. *) diff --git a/matita/matita/lib/hott/notations.ma b/matita/matita/lib/hott/notations.ma index 83d3324ae..71d41f73b 100644 --- a/matita/matita/lib/hott/notations.ma +++ b/matita/matita/lib/hott/notations.ma @@ -243,10 +243,6 @@ for @{ 'divide $a $b }. notation "- term 65 a" with precedence 65 for @{ 'uminus $a }. -notation "a !" - non associative with precedence 80 -for @{ 'fact $a }. - notation "\sqrt a" non associative with precedence 65 for @{ 'sqrt $a }. @@ -277,18 +273,6 @@ for @{ 'powerset $A }. notation > "hvbox(\Omega ^ term 90 A)" non associative with precedence 90 for @{ 'powerset $A }. -notation < "hvbox({ ident i | term 19 p })" with precedence 90 -for @{ 'subset (\lambda ${ident i} : $nonexistent . $p)}. - -notation > "hvbox({ ident i | term 19 p })" with precedence 90 -for @{ 'subset (\lambda ${ident i}. $p)}. - -notation < "hvbox({ ident i ∈ term 19 s | term 19 p })" with precedence 90 -for @{ 'comprehension $s (\lambda ${ident i} : $nonexistent . $p)}. - -notation > "hvbox({ ident i ∈ term 19 s | term 19 p })" with precedence 90 -for @{ 'comprehension $s (\lambda ${ident i}. $p)}. - notation "hvbox(a break ∈ b)" non associative with precedence 45 for @{ 'mem $a $b }. @@ -307,20 +291,12 @@ for @{ 'intersects $a $b }. (* \cap *) 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}. - notation "hvbox(a break \approx b)" non associative with precedence 45 for @{ 'napart $a $b}. notation "hvbox(a break # b)" non associative with precedence 45 for @{ 'apart $a $b}. -*) - -notation "hvbox(a break \circ b)" - left associative with precedence 60 -for @{ 'compose $a $b }. -(* notation < "↓ \ensp a" with precedence 60 for @{ 'downarrow $a }. notation > "↓ a" with precedence 60 for @{ 'downarrow $a }. diff --git a/matita/matita/lib/re/reb.ma b/matita/matita/lib/re/reb.ma index 73faed377..2c5b129d2 100644 --- a/matita/matita/lib/re/reb.ma +++ b/matita/matita/lib/re/reb.ma @@ -14,6 +14,7 @@ include "arithmetics/nat.ma". include "basics/lists/list.ma". +include "basics/core_notation/singl_1.ma". interpretation "iff" 'iff a b = (iff a b). @@ -778,4 +779,4 @@ ntheorem der1: ∀S,a,e,e',w. der S a e e' → in_l S w e' → in_l S (a::w) e. | #x; #y; #z; #w; #a; #b; #c; #d; #K; ncases (?:False); /2/ ] ##| #r1; #r2; #r1'; #r2'; #H1; #H2; #H3; #H4; #H5; #H6; -*) \ No newline at end of file +*) diff --git a/matita/matita/lib/turing/wmono.ma b/matita/matita/lib/turing/wmono.ma index 35c409639..d31ed62f5 100644 --- a/matita/matita/lib/turing/wmono.ma +++ b/matita/matita/lib/turing/wmono.ma @@ -11,6 +11,7 @@ include "basics/vectors.ma". include "basics/finset.ma". +include "basics/core_notation/compose_2.ma". (* include "basics/relations.ma". *) record tape (sig:FinSet): Type[0] ≝ diff --git a/matita/matita/lib/tutorial/chapter6.ma b/matita/matita/lib/tutorial/chapter6.ma index 38fb54a0c..a5355b5fa 100644 --- a/matita/matita/lib/tutorial/chapter6.ma +++ b/matita/matita/lib/tutorial/chapter6.ma @@ -1,5 +1,6 @@ include "tutorial/chapter5.ma". +include "basics/core_notation/singl_1.ma". (*************************** Naive Set Theory *********************************) -- 2.39.2