From bd840d43d09254b41936c49fc447e58582b156eb Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 16 May 2019 23:55:15 +0200 Subject: [PATCH] decentralizing core notation continues ... + apart, napart decentralized --- matita/matita/lib/basics/core_notation.ma | 6 ------ matita/matita/lib/basics/core_notation/apart_2.ma | 15 +++++++++++++++ .../matita/lib/basics/core_notation/napart_2.ma | 15 +++++++++++++++ matita/matita/lib/pts_dummy/rc_eval.ma | 1 + matita/matita/lib/pts_dummy_new/rc_eval.ma | 1 + .../matita/lib/reverse_complexity/speed_clean.ma | 3 ++- matita/matita/lib/reverse_complexity/speed_def.ma | 3 ++- matita/matita/lib/reverse_complexity/speed_new.ma | 3 ++- matita/matita/lib/reverse_complexity/toolkit.ma | 3 ++- 9 files changed, 40 insertions(+), 10 deletions(-) create mode 100644 matita/matita/lib/basics/core_notation/apart_2.ma create mode 100644 matita/matita/lib/basics/core_notation/napart_2.ma diff --git a/matita/matita/lib/basics/core_notation.ma b/matita/matita/lib/basics/core_notation.ma index 3bf1de3b2..4d1e355a3 100644 --- a/matita/matita/lib/basics/core_notation.ma +++ b/matita/matita/lib/basics/core_notation.ma @@ -280,12 +280,6 @@ for @{ 'union $a $b }. (* \cup *) (* other notations **********************************************************) -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 < "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}. notation > "a ^ term 90 b" non associative with precedence 75 for @{ 'exp $a $b}. diff --git a/matita/matita/lib/basics/core_notation/apart_2.ma b/matita/matita/lib/basics/core_notation/apart_2.ma new file mode 100644 index 000000000..04c81ec27 --- /dev/null +++ b/matita/matita/lib/basics/core_notation/apart_2.ma @@ -0,0 +1,15 @@ +(* + ||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 # b)" non associative with precedence 45 + for @{ 'apart $a $b}. diff --git a/matita/matita/lib/basics/core_notation/napart_2.ma b/matita/matita/lib/basics/core_notation/napart_2.ma new file mode 100644 index 000000000..a3817876b --- /dev/null +++ b/matita/matita/lib/basics/core_notation/napart_2.ma @@ -0,0 +1,15 @@ +(* + ||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 \approx b)" non associative with precedence 45 + for @{ 'napart $a $b}. diff --git a/matita/matita/lib/pts_dummy/rc_eval.ma b/matita/matita/lib/pts_dummy/rc_eval.ma index 87cfd11dc..439160a7d 100644 --- a/matita/matita/lib/pts_dummy/rc_eval.ma +++ b/matita/matita/lib/pts_dummy/rc_eval.ma @@ -13,6 +13,7 @@ (**************************************************************************) include "pts_dummy/rc_hsat.ma". +include "basics/core_notation/napart_2.ma". (* (* THE EVALUATION *************************************************************) diff --git a/matita/matita/lib/pts_dummy_new/rc_eval.ma b/matita/matita/lib/pts_dummy_new/rc_eval.ma index 7b7ce54d9..c11eca57a 100644 --- a/matita/matita/lib/pts_dummy_new/rc_eval.ma +++ b/matita/matita/lib/pts_dummy_new/rc_eval.ma @@ -13,6 +13,7 @@ (**************************************************************************) include "pts_dummy/rc_hsat.ma". +include "basics/core_notation/napart_2.ma". (* (* THE EVALUATION *************************************************************) diff --git a/matita/matita/lib/reverse_complexity/speed_clean.ma b/matita/matita/lib/reverse_complexity/speed_clean.ma index 9b9fecf94..bfd3d34b1 100644 --- a/matita/matita/lib/reverse_complexity/speed_clean.ma +++ b/matita/matita/lib/reverse_complexity/speed_clean.ma @@ -4,6 +4,7 @@ include "arithmetics/bigops.ma". include "arithmetics/sigma_pi.ma". include "arithmetics/bounded_quantifiers.ma". include "reverse_complexity/big_O.ma". +include "basics/core_notation/napart_2.ma". (************************* notation for minimization *****************************) notation "μ_{ ident i < n } p" @@ -1064,4 +1065,4 @@ lapply (speed_compl_i … Hr Hmono Hconstr (S i)) #Hg @Hmono @(mono_h_of2 … Hr Hmono … ltin) ] qed. - \ No newline at end of file + diff --git a/matita/matita/lib/reverse_complexity/speed_def.ma b/matita/matita/lib/reverse_complexity/speed_def.ma index 6a0ec4a57..9812cfb08 100644 --- a/matita/matita/lib/reverse_complexity/speed_def.ma +++ b/matita/matita/lib/reverse_complexity/speed_def.ma @@ -4,6 +4,7 @@ include "arithmetics/bigops.ma". include "arithmetics/sigma_pi.ma". include "arithmetics/bounded_quantifiers.ma". include "reverse_complexity/big_O.ma". +include "basics/core_notation/napart_2.ma". (************************* notation for minimization *****************************) notation "μ_{ ident i < n } p" @@ -918,4 +919,4 @@ lapply (speed_compl_i … Hr Hmono Hconstr (S i)) #Hg @Hmono @(mono_h_of2 … Hr Hmono … ltin) ] qed. - \ No newline at end of file + diff --git a/matita/matita/lib/reverse_complexity/speed_new.ma b/matita/matita/lib/reverse_complexity/speed_new.ma index 6a0ec4a57..9812cfb08 100644 --- a/matita/matita/lib/reverse_complexity/speed_new.ma +++ b/matita/matita/lib/reverse_complexity/speed_new.ma @@ -4,6 +4,7 @@ include "arithmetics/bigops.ma". include "arithmetics/sigma_pi.ma". include "arithmetics/bounded_quantifiers.ma". include "reverse_complexity/big_O.ma". +include "basics/core_notation/napart_2.ma". (************************* notation for minimization *****************************) notation "μ_{ ident i < n } p" @@ -918,4 +919,4 @@ lapply (speed_compl_i … Hr Hmono Hconstr (S i)) #Hg @Hmono @(mono_h_of2 … Hr Hmono … ltin) ] qed. - \ No newline at end of file + diff --git a/matita/matita/lib/reverse_complexity/toolkit.ma b/matita/matita/lib/reverse_complexity/toolkit.ma index 11f988c79..69fa3525a 100644 --- a/matita/matita/lib/reverse_complexity/toolkit.ma +++ b/matita/matita/lib/reverse_complexity/toolkit.ma @@ -4,6 +4,7 @@ include "arithmetics/bigops.ma". include "arithmetics/sigma_pi.ma". include "arithmetics/bounded_quantifiers.ma". include "reverse_complexity/big_O.ma". +include "basics/core_notation/napart_2.ma". (************************* notation for minimization *****************************) notation "μ_{ ident i < n } p" @@ -984,4 +985,4 @@ lapply (speed_compl_i … Hr Hmono Hconstr (S i)) #Hg @Hmono @(mono_h_of2 … Hr Hmono … ltin) ] qed. - \ No newline at end of file + -- 2.39.2