From 24ba1bb3f67505d3e384747ff90d26d3996bd3f5 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 20 Apr 2018 17:47:08 +0200 Subject: [PATCH] decentralizing core notation continues ... + uparrows and downarrows clash with \lambda\delta + improved list of failing files --- matita/matita/lib/basics/core_notation.ma | 9 ------ .../lib/basics/core_notation/downarrow_1.ma | 16 ++++++++++ .../lib/basics/core_notation/fintersects_2.ma | 14 +++++++++ .../lib/basics/core_notation/funion_2.ma | 14 +++++++++ .../lib/basics/core_notation/uparrow_1.ma | 14 +++++++++ matita/matita/lib/fail.txt | 30 +++++-------------- .../matita/lib/formal_topology/basic_pairs.ma | 1 + .../lib/formal_topology/formal_topologies.ma | 2 ++ .../lib/formal_topology/o-basic_pairs.ma | 1 + .../lib/formal_topology/o-concrete_spaces.ma | 2 ++ .../formal_topology/o-formal_topologies.ma | 2 ++ matita/matita/lib/hott/notations.ma | 9 ------ matita/matita/lib/turing/mono.ma | 1 + matita/matita/lib/turing/turing.ma | 1 + 14 files changed, 75 insertions(+), 41 deletions(-) create mode 100644 matita/matita/lib/basics/core_notation/downarrow_1.ma create mode 100644 matita/matita/lib/basics/core_notation/fintersects_2.ma create mode 100644 matita/matita/lib/basics/core_notation/funion_2.ma create mode 100644 matita/matita/lib/basics/core_notation/uparrow_1.ma diff --git a/matita/matita/lib/basics/core_notation.ma b/matita/matita/lib/basics/core_notation.ma index cdc535b81..a0ad502b9 100644 --- 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 index 000000000..717f0ee32 --- /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 index 000000000..d5d270d44 --- /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 index 000000000..56a83dbbf --- /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 index 000000000..a81bb142e --- /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 4330dddb1..6da43596d 100644 --- 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 ded2eb517..941175c31 100644 --- 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 e3af412e3..84cd97c20 100644 --- 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 1e01764a7..a0c378b20 100644 --- 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 f39b25109..2e8b8ad8b 100644 --- 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 489aba016..9ef52e517 100644 --- 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 71d41f73b..d71589e2a 100644 --- 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 393fa2af9..3477508c1 100644 --- 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 9b2d8437c..dc0a43e75 100644 --- 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". -- 2.39.2