From e8571cfbc30a3da656cff0c0e0f0ee747e8c4cdd Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 8 Jan 2022 22:24:10 +0100 Subject: [PATCH] update in lib + notation for card decentralized --- matita/matita/lib/basics/core_notation.ma | 2 -- matita/matita/lib/basics/core_notation/card_1.ma | 14 ++++++++++++++ matita/matita/lib/basics/lists/list.ma | 1 + matita/matita/lib/hott/notations.ma | 2 -- matita/matita/lib/lambda/paths/decomposed_trace.ma | 1 + matita/matita/lib/lambda/terms/size.ma | 1 + matita/matita/lib/re/re.ma | 1 + matita/matita/lib/reverse_complexity/hierarchy.ma | 3 ++- matita/matita/lib/tutorial/chapter5.ma | 2 +- matita/matita/lib/tutorial/chapter8.ma | 1 + 10 files changed, 22 insertions(+), 6 deletions(-) create mode 100644 matita/matita/lib/basics/core_notation/card_1.ma diff --git a/matita/matita/lib/basics/core_notation.ma b/matita/matita/lib/basics/core_notation.ma index 54bfd22d5..52ca7e961 100644 --- a/matita/matita/lib/basics/core_notation.ma +++ b/matita/matita/lib/basics/core_notation.ma @@ -277,8 +277,6 @@ for @{ 'union $a $b }. (* \cup *) (* other notations **********************************************************) -notation "| term 19 C |" with precedence 70 for @{ 'card $C }. - notation "\naturals" non associative with precedence 90 for @{'N}. notation "\rationals" non associative with precedence 90 for @{'Q}. notation "\reals" non associative with precedence 90 for @{'R}. diff --git a/matita/matita/lib/basics/core_notation/card_1.ma b/matita/matita/lib/basics/core_notation/card_1.ma new file mode 100644 index 000000000..232493564 --- /dev/null +++ b/matita/matita/lib/basics/core_notation/card_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 "| term 19 C |" with precedence 70 for @{ 'card $C }. diff --git a/matita/matita/lib/basics/lists/list.ma b/matita/matita/lib/basics/lists/list.ma index f8c2ac772..ed988b760 100644 --- a/matita/matita/lib/basics/lists/list.ma +++ b/matita/matita/lib/basics/lists/list.ma @@ -11,6 +11,7 @@ include "basics/types.ma". include "arithmetics/nat.ma". +include "basics/core_notation/card_1.ma". inductive list (A:Type[0]) : Type[0] := | nil: list A diff --git a/matita/matita/lib/hott/notations.ma b/matita/matita/lib/hott/notations.ma index 09a8c37cc..d680e4bd1 100644 --- a/matita/matita/lib/hott/notations.ma +++ b/matita/matita/lib/hott/notations.ma @@ -302,8 +302,6 @@ notation "s ^ (-1)" non associative with precedence 75 for @{ 'invert $s }. (* notation < "s \sup (-1) x" non associative with precedence 90 for @{ 'invert_appl $s $x}. -notation "| term 19 C |" with precedence 70 for @{ 'card $C }. - notation "\naturals" non associative with precedence 90 for @{'N}. notation "\rationals" non associative with precedence 90 for @{'Q}. notation "\reals" non associative with precedence 90 for @{'R}. diff --git a/matita/matita/lib/lambda/paths/decomposed_trace.ma b/matita/matita/lib/lambda/paths/decomposed_trace.ma index 9c391c1a9..1e6ae78de 100644 --- a/matita/matita/lib/lambda/paths/decomposed_trace.ma +++ b/matita/matita/lib/lambda/paths/decomposed_trace.ma @@ -13,6 +13,7 @@ (**************************************************************************) include "lambda/paths/trace.ma". +include "basics/core_notation/card_1.ma". (* DECOMPOSED TRACE *********************************************************) diff --git a/matita/matita/lib/lambda/terms/size.ma b/matita/matita/lib/lambda/terms/size.ma index 3396dc415..a07112701 100644 --- a/matita/matita/lib/lambda/terms/size.ma +++ b/matita/matita/lib/lambda/terms/size.ma @@ -13,6 +13,7 @@ (**************************************************************************) include "lambda/terms/relocation.ma". +include "basics/core_notation/card_1.ma". (* SIZE *********************************************************************) diff --git a/matita/matita/lib/re/re.ma b/matita/matita/lib/re/re.ma index 234d522ae..8ba714b82 100644 --- a/matita/matita/lib/re/re.ma +++ b/matita/matita/lib/re/re.ma @@ -13,6 +13,7 @@ (**************************************************************************) include "re/lang.ma". +include "basics/core_notation/card_1.ma". (* The type re of regular expressions over an alphabet $S$ is the smallest collection of objects generated by the following constructors: *) diff --git a/matita/matita/lib/reverse_complexity/hierarchy.ma b/matita/matita/lib/reverse_complexity/hierarchy.ma index d833a5164..cae93c256 100644 --- a/matita/matita/lib/reverse_complexity/hierarchy.ma +++ b/matita/matita/lib/reverse_complexity/hierarchy.ma @@ -6,6 +6,7 @@ include "arithmetics/bounded_quantifiers.ma". include "arithmetics/pidgeon_hole.ma". include "basics/sets.ma". include "basics/types.ma". +include "basics/core_notation/card_1.ma". (************************************ MAX *************************************) notation "Max_{ ident i < n | p } f" @@ -468,4 +469,4 @@ cut (O (λx:ℕ.sU x x (s x)) s) [%{1} %{0} #n //] |%{1} %{0} #n #_ >commutative_times size_f_size >size_of_size // ] -qed. \ No newline at end of file +qed. diff --git a/matita/matita/lib/tutorial/chapter5.ma b/matita/matita/lib/tutorial/chapter5.ma index 21a8abd2f..b1493982c 100644 --- a/matita/matita/lib/tutorial/chapter5.ma +++ b/matita/matita/lib/tutorial/chapter5.ma @@ -4,7 +4,7 @@ include "tutorial/chapter4.ma". include "arithmetics/nat.ma". - +include "basics/core_notation/card_1.ma". (******************************** Option Type *********************************) diff --git a/matita/matita/lib/tutorial/chapter8.ma b/matita/matita/lib/tutorial/chapter8.ma index 427b14842..47cfbdeb7 100644 --- a/matita/matita/lib/tutorial/chapter8.ma +++ b/matita/matita/lib/tutorial/chapter8.ma @@ -5,6 +5,7 @@ We shall apply all the previous machinery to the study of regular languages and the constructions of the associated finite automata. *) include "tutorial/chapter7.ma". +include "basics/core_notation/card_1.ma". (* The type re of regular expressions over an alphabet $S$ is the smallest collection of objects generated by the following constructors: *) -- 2.39.2