From: Ferruccio Guidi <fguidi@maelstrom.helm.cs.unibo.it>
Date: Thu, 5 Mar 2020 14:16:35 +0000 (+0100)
Subject: update in standard library
X-Git-Tag: make_still_working~185
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=84b38ac86f1f92b91ae8913cd0dbcb5c3485dc3a;p=helm.git

update in standard library

+ some notations with ^ decentralized
+ one decentralized notation added to reverse_complexity/speedup.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 **********************)