From 84b38ac86f1f92b91ae8913cd0dbcb5c3485dc3a Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 5 Mar 2020 15:16:35 +0100 Subject: [PATCH] update in standard library + some notations with ^ decentralized + one decentralized notation added to reverse_complexity/speedup.ma --- matita/matita/lib/arithmetics/exp.ma | 3 ++- matita/matita/lib/arithmetics/iteration.ma | 3 ++- matita/matita/lib/basics/core_notation.ma | 7 ------- matita/matita/lib/basics/core_notation/exp_2.ma | 16 ++++++++++++++++ .../matita/lib/basics/core_notation/invert_1.ma | 15 +++++++++++++++ .../lib/basics/core_notation/invert_appl_2.ma | 14 ++++++++++++++ matita/matita/lib/formal_topology/categories.ma | 1 + matita/matita/lib/reverse_complexity/speedup.ma | 3 ++- matita/matita/lib/tutorial/chapter12.ma | 1 + 9 files changed, 53 insertions(+), 10 deletions(-) create mode 100644 matita/matita/lib/basics/core_notation/exp_2.ma create mode 100644 matita/matita/lib/basics/core_notation/invert_1.ma create mode 100644 matita/matita/lib/basics/core_notation/invert_appl_2.ma diff --git a/matita/matita/lib/arithmetics/exp.ma b/matita/matita/lib/arithmetics/exp.ma index 654185c89..5c7500dd9 100644 --- a/matita/matita/lib/arithmetics/exp.ma +++ b/matita/matita/lib/arithmetics/exp.ma @@ -10,6 +10,7 @@ V_______________________________________________________________ *) include "arithmetics/div_and_mod.ma". +include "basics/core_notation/exp_2.ma". let rec exp n m on m ≝ match m with @@ -182,4 +183,4 @@ qed. - \ No newline at end of file + diff --git a/matita/matita/lib/arithmetics/iteration.ma b/matita/matita/lib/arithmetics/iteration.ma index 78d4eb4d0..407e12b03 100644 --- a/matita/matita/lib/arithmetics/iteration.ma +++ b/matita/matita/lib/arithmetics/iteration.ma @@ -10,6 +10,7 @@ V_______________________________________________________________ *) include "arithmetics/nat.ma". +include "basics/core_notation/exp_2.ma". (* iteration *) @@ -43,4 +44,4 @@ lemma monotonic_iter2: ∀g,a,i,j. (∀x. x ≤ g x) → i ≤ j → g^i a ≤ g^j a. #g #a #i #j #leg #leij elim leij // #m #leim #Hind normalize @(transitive_le … Hind) @leg -qed. \ No newline at end of file +qed. diff --git a/matita/matita/lib/basics/core_notation.ma b/matita/matita/lib/basics/core_notation.ma index 4d1e355a3..4ed9f326c 100644 --- a/matita/matita/lib/basics/core_notation.ma +++ b/matita/matita/lib/basics/core_notation.ma @@ -280,13 +280,6 @@ for @{ 'union $a $b }. (* \cup *) (* other notations **********************************************************) -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}. -notation "s \sup (-1)" non associative with precedence 75 for @{ 'invert $s }. -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}. diff --git a/matita/matita/lib/basics/core_notation/exp_2.ma b/matita/matita/lib/basics/core_notation/exp_2.ma new file mode 100644 index 000000000..c5cd9ddbb --- /dev/null +++ b/matita/matita/lib/basics/core_notation/exp_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 < "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/invert_1.ma b/matita/matita/lib/basics/core_notation/invert_1.ma new file mode 100644 index 000000000..14f5692f5 --- /dev/null +++ b/matita/matita/lib/basics/core_notation/invert_1.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 "s \sup (-1)" non associative with precedence 75 for @{ 'invert $s }. +notation > "s ^ (-1)" non associative with precedence 75 for @{ 'invert $s }. diff --git a/matita/matita/lib/basics/core_notation/invert_appl_2.ma b/matita/matita/lib/basics/core_notation/invert_appl_2.ma new file mode 100644 index 000000000..57a9eebfa --- /dev/null +++ b/matita/matita/lib/basics/core_notation/invert_appl_2.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 < "s \sup (-1) x" non associative with precedence 90 for @{ 'invert_appl $s $x}. diff --git a/matita/matita/lib/formal_topology/categories.ma b/matita/matita/lib/formal_topology/categories.ma index 02605e4a8..94a8d22eb 100644 --- a/matita/matita/lib/formal_topology/categories.ma +++ b/matita/matita/lib/formal_topology/categories.ma @@ -14,6 +14,7 @@ include "formal_topology/cprop_connectives.ma". include "basics/core_notation/compose_2.ma". +include "basics/core_notation/invert_1.ma". inductive eq (A:Type[0]) (x:A) : A → CProp[0] ≝ refl: eq A x x. diff --git a/matita/matita/lib/reverse_complexity/speedup.ma b/matita/matita/lib/reverse_complexity/speedup.ma index f1e56d560..52b7db0dd 100644 --- a/matita/matita/lib/reverse_complexity/speedup.ma +++ b/matita/matita/lib/reverse_complexity/speedup.ma @@ -1,4 +1,5 @@ include "reverse_complexity/bigops_compl.ma". +include "basics/core_notation/napart_2.ma". (********************************* the speedup ********************************) @@ -569,4 +570,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/tutorial/chapter12.ma b/matita/matita/lib/tutorial/chapter12.ma index 72e396c13..07a5fd19f 100644 --- a/matita/matita/lib/tutorial/chapter12.ma +++ b/matita/matita/lib/tutorial/chapter12.ma @@ -16,6 +16,7 @@ include "basics/relations.ma". include "basics/types.ma". include "arithmetics/nat.ma". include "hints_declaration.ma". +include "basics/core_notation/invert_1.ma". (******************* Quotienting in type theory **********************) -- 2.39.2