From: Ferruccio Guidi Date: Thu, 16 May 2019 21:55:15 +0000 (+0200) Subject: decentralizing core notation continues ... X-Git-Tag: make_still_working~249 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=bd840d43d09254b41936c49fc447e58582b156eb decentralizing core notation continues ... + apart, napart decentralized --- 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 +