decentralizing core notation continues ...

+ uparrows and downarrows clash with \lambda\delta
+ improved list of failing files

diff --git a/matita/matita/lib/basics/core_notation.ma b/matita/matita/lib/basics/core_notation.ma
index cdc535b81de67c9f0233fe588afcc65ddb98f230..a0ad502b942165237493cac0375c010cb08a4dd0 100644 (file)
--- a/matita/matita/lib/basics/core_notation.ma
+++ b/matita/matita/lib/basics/core_notation.ma
@@ -289,15 +289,6 @@ notation "hvbox(a break \approx b)" non associative with precedence 45
 notation "hvbox(a break # b)" non associative with precedence 45 
   for @{ 'apart $a $b}.
 
-notation < "↓ \ensp a" with precedence 60 for @{ 'downarrow $a }.
-notation > "↓ a" with precedence 60 for @{ 'downarrow $a }.
-
-notation "hvbox(U break ↓ V)" non associative with precedence 60 for @{ 'fintersects $U $V }.
-
-notation "↑a" with precedence 60 for @{ 'uparrow $a }.
-
-notation "hvbox(a break ↑ b)" with precedence 60 for @{ 'funion $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/downarrow_1.ma b/matita/matita/lib/basics/core_notation/downarrow_1.ma
new file mode 100644 (file)
index 0000000..717f0ee
--- /dev/null
+++ b/matita/matita/lib/basics/core_notation/downarrow_1.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 < "↓ \ensp a" with precedence 60 for @{ 'downarrow $a }.
+
+notation > "↓ a" with precedence 60 for @{ 'downarrow $a }.

diff --git a/matita/matita/lib/basics/core_notation/fintersects_2.ma b/matita/matita/lib/basics/core_notation/fintersects_2.ma
new file mode 100644 (file)
index 0000000..d5d270d
--- /dev/null
+++ b/matita/matita/lib/basics/core_notation/fintersects_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 "hvbox(U break ↓ V)" non associative with precedence 60 for @{ 'fintersects $U $V }.

diff --git a/matita/matita/lib/basics/core_notation/funion_2.ma b/matita/matita/lib/basics/core_notation/funion_2.ma
new file mode 100644 (file)
index 0000000..56a83db
--- /dev/null
+++ b/matita/matita/lib/basics/core_notation/funion_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 "hvbox(a break ↑ b)" with precedence 60 for @{ 'funion $a $b }.

diff --git a/matita/matita/lib/basics/core_notation/uparrow_1.ma b/matita/matita/lib/basics/core_notation/uparrow_1.ma
new file mode 100644 (file)
index 0000000..a81bb14
--- /dev/null
+++ b/matita/matita/lib/basics/core_notation/uparrow_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 "↑a" with precedence 60 for @{ 'uparrow $a }.

diff --git a/matita/matita/lib/fail.txt b/matita/matita/lib/fail.txt
index 4330dddb10746a70efb8dba128b489d67f704868..6da43596dafbc1360684b11cccf84006d731c6f5 100644 (file)
--- a/matita/matita/lib/fail.txt
+++ b/matita/matita/lib/fail.txt
@@ -1,27 +1,11 @@
-matitac.opt turing/multi_to_mono/multi_to_mono.maFAIL 0m00.54s 0m00.52s 0m00.01s 
-matitac.opt binding/names.ma                     FAIL 0m00.07s 0m00.07s 0m00.00s 
 matitac.opt binding/fp.ma
- matitac.opt binding/names.ma                    FAIL 0m00.12s 0m00.12s 0m00.00s 
-matitac.opt binding/fp.ma                        FAIL 0m00.13s 0m00.12s 0m00.00s 
-matitac.opt binding/ln.ma
- matitac.opt binding/names.ma                    FAIL 0m00.07s 0m00.07s 0m00.00s 
-matitac.opt binding/ln.ma                        FAIL 0m00.43s 0m00.43s 0m00.00s 
 matitac.opt binding/ln_concrete.ma
- matitac.opt binding/names.ma                    FAIL 0m00.06s 0m00.06s 0m00.00s 
-matitac.opt binding/ln_concrete.ma               FAIL 0m00.49s 0m00.48s 0m00.00s 
+matitac.opt binding/ln.ma
+matitac.opt binding/names.ma
+matitac.opt finite_lambda/confluence.ma
 matitac.opt finite_lambda/reduction.ma
- matitac.opt finite_lambda/terms_and_types.ma    FAIL 0m00.47s 0m00.47s 0m00.00s 
-matitac.opt finite_lambda/reduction.ma           FAIL 0m00.48s 0m00.47s 0m00.00s 
+matitac.opt finite_lambda/terms_and_types.ma
 matitac.opt finite_lambda/typing.ma
- matitac.opt finite_lambda/reduction.ma
-  matitac.opt finite_lambda/terms_and_types.ma   FAIL 0m00.39s 0m00.39s 0m00.00s 
- matitac.opt finite_lambda/reduction.ma          FAIL 0m00.39s 0m00.39s 0m00.00s 
-matitac.opt finite_lambda/typing.ma              FAIL 0m00.39s 0m00.39s 0m00.00s 
-matitac.opt finite_lambda/confluence.ma
- matitac.opt finite_lambda/reduction.ma
-  matitac.opt finite_lambda/terms_and_types.ma   FAIL 0m00.42s 0m00.41s 0m00.00s 
- matitac.opt finite_lambda/reduction.ma          FAIL 0m00.42s 0m00.42s 0m00.00s 
-matitac.opt finite_lambda/confluence.ma          FAIL 0m00.42s 0m00.42s 0m00.00s 
-matitac.opt finite_lambda/terms_and_types.ma     FAIL 0m00.38s 0m00.38s 0m00.00s 
-matitac.opt reverse_complexity/toolkit.ma        FAIL 0m14.70s 0m14.62s 0m00.07s 
-matitac.opt reverse_complexity/hierarchy.ma      FAIL 0m00.71s 0m00.70s 0m00.00s 
+matitac.opt reverse_complexity/hierarchy.ma
+matitac.opt reverse_complexity/toolkit.ma
+matitac.opt turing/multi_to_mono/multi_to_mono.ma

diff --git a/matita/matita/lib/formal_topology/basic_pairs.ma b/matita/matita/lib/formal_topology/basic_pairs.ma
index ded2eb517826d3a1af07aeb718c26a0cec2c7f72..941175c31ff00b62e6709757700db91262027752 100644 (file)
--- a/matita/matita/lib/formal_topology/basic_pairs.ma
+++ b/matita/matita/lib/formal_topology/basic_pairs.ma
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "basics/core_notation/fintersects_2.ma".
 include "formal_topology/relations.ma".
 include "formal_topology/notation.ma".
 (*

diff --git a/matita/matita/lib/formal_topology/formal_topologies.ma b/matita/matita/lib/formal_topology/formal_topologies.ma
index e3af412e31f519293d57822d5898956de6b2e9d5..84cd97c206ca44fd68a8b642a37dc0fff81df570 100644 (file)
--- a/matita/matita/lib/formal_topology/formal_topologies.ma
+++ b/matita/matita/lib/formal_topology/formal_topologies.ma
@@ -12,6 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "basics/core_notation/fintersects_2.ma".
+include "basics/core_notation/downarrow_1.ma".
 include "formal_topology/basic_topologies.ma".
 (*
 (*

diff --git a/matita/matita/lib/formal_topology/o-basic_pairs.ma b/matita/matita/lib/formal_topology/o-basic_pairs.ma
index 1e01764a7ce1d9f970c8ce312bc562a9aa94ca22..a0c378b2044f5d1b4d1d5ddf5fbd84789e01639c 100644 (file)
--- a/matita/matita/lib/formal_topology/o-basic_pairs.ma
+++ b/matita/matita/lib/formal_topology/o-basic_pairs.ma
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "basics/core_notation/fintersects_2.ma".
 include "formal_topology/o-algebra.ma".
 include "formal_topology/notation.ma".
 (*

diff --git a/matita/matita/lib/formal_topology/o-concrete_spaces.ma b/matita/matita/lib/formal_topology/o-concrete_spaces.ma
index f39b25109c5655d5097278593464637143a11fa8..2e8b8ad8b34671bde2fbfa90e1904304d794c6ad 100644 (file)
--- a/matita/matita/lib/formal_topology/o-concrete_spaces.ma
+++ b/matita/matita/lib/formal_topology/o-concrete_spaces.ma
@@ -12,6 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "basics/core_notation/fintersects_2.ma".
+include "basics/core_notation/downarrow_1.ma".
 include "formal_topology/o-basic_pairs.ma".
 include "formal_topology/o-saturations.ma".
 (*

diff --git a/matita/matita/lib/formal_topology/o-formal_topologies.ma b/matita/matita/lib/formal_topology/o-formal_topologies.ma
index 489aba0166b1a79ce00ec5b2eccab74df75ae4e7..9ef52e517f5a5a40f9fad474c827476c038581db 100644 (file)
--- a/matita/matita/lib/formal_topology/o-formal_topologies.ma
+++ b/matita/matita/lib/formal_topology/o-formal_topologies.ma
@@ -12,6 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "basics/core_notation/fintersects_2.ma".
+include "basics/core_notation/downarrow_1.ma".
 include "formal_topology/o-basic_topologies.ma".
 (*
 (*

diff --git a/matita/matita/lib/hott/notations.ma b/matita/matita/lib/hott/notations.ma
index 71d41f73b061d0ef3f982298a0777c5f025cfde8..d71589e2a98cf324146388cc5c9218b1de8677ad 100644 (file)
--- a/matita/matita/lib/hott/notations.ma
+++ b/matita/matita/lib/hott/notations.ma
@@ -297,15 +297,6 @@ notation "hvbox(a break \approx b)" non associative with precedence 45
 notation "hvbox(a break # b)" non associative with precedence 45 
   for @{ 'apart $a $b}.
 
-notation < "↓ \ensp a" with precedence 60 for @{ 'downarrow $a }.
-notation > "↓ a" with precedence 60 for @{ 'downarrow $a }.
-
-notation "hvbox(U break ↓ V)" non associative with precedence 60 for @{ 'fintersects $U $V }.
-
-notation "↑a" with precedence 60 for @{ 'uparrow $a }.
-
-notation "hvbox(a break ↑ b)" with precedence 60 for @{ 'funion $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/turing/mono.ma b/matita/matita/lib/turing/mono.ma
index 393fa2af92784c68e38354c25cdc0d4d2fbaa1b2..3477508c15528dad59bdc44fd0cc654db3e4ab20 100644 (file)
--- a/matita/matita/lib/turing/mono.ma
+++ b/matita/matita/lib/turing/mono.ma
@@ -9,6 +9,7 @@
      \ /   GNU General Public License Version 2   
       V_____________________________________________________________*)
 
+include "basics/core_notation/fintersects_2.ma".
 include "basics/finset.ma".
 include "basics/vectors.ma".
 include "basics/finset.ma".

diff --git a/matita/matita/lib/turing/turing.ma b/matita/matita/lib/turing/turing.ma
index 9b2d8437c32605d0604dbefb8fde2d37368ff72b..dc0a43e755968a27ea32aaea3deb2fa84548a03d 100644 (file)
--- a/matita/matita/lib/turing/turing.ma
+++ b/matita/matita/lib/turing/turing.ma
@@ -1,3 +1,4 @@
+include "basics/core_notation/fintersects_2.ma".
 include "turing/mono.ma".
 include "basics/vectors.ma".