From 969cce2e68f83cfc3fdfc13b6cea4c920d7c51d5 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 8 Jun 2022 19:49:26 +0200 Subject: [PATCH] update in lib + notation for overlap decentralized --- matita/matita/lib/basics/core_notation.ma | 3 --- .../matita/lib/basics/core_notation/overlaps_2.ma | 15 +++++++++++++++ matita/matita/lib/hott/notations.ma | 6 ------ 3 files changed, 15 insertions(+), 9 deletions(-) create mode 100644 matita/matita/lib/basics/core_notation/overlaps_2.ma diff --git a/matita/matita/lib/basics/core_notation.ma b/matita/matita/lib/basics/core_notation.ma index 52ca7e961..0a1c3fd80 100644 --- a/matita/matita/lib/basics/core_notation.ma +++ b/matita/matita/lib/basics/core_notation.ma @@ -266,9 +266,6 @@ for @{ 'mem $a $b }. notation "hvbox(a break ∉ b)" non associative with precedence 45 for @{ 'notmem $a $b }. -notation "hvbox(a break ≬ b)" non associative with precedence 45 -for @{ 'overlaps $a $b }. (* \between *) - notation "hvbox(a break ∩ b)" left associative with precedence 60 for @{ 'intersects $a $b }. (* \cap *) diff --git a/matita/matita/lib/basics/core_notation/overlaps_2.ma b/matita/matita/lib/basics/core_notation/overlaps_2.ma new file mode 100644 index 000000000..0dafc5c96 --- /dev/null +++ b/matita/matita/lib/basics/core_notation/overlaps_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 @{ 'overlaps $a $b }. (* \between *) diff --git a/matita/matita/lib/hott/notations.ma b/matita/matita/lib/hott/notations.ma index d680e4bd1..d2d843cf0 100644 --- a/matita/matita/lib/hott/notations.ma +++ b/matita/matita/lib/hott/notations.ma @@ -276,12 +276,6 @@ for @{ 'mem $a $b }. notation "hvbox(a break ∉ b)" non associative with precedence 45 for @{ 'notmem $a $b }. -notation "hvbox(a break ≬ b)" non associative with precedence 45 -for @{ 'overlaps $a $b }. (* \between *) - -notation "hvbox(a break ⊆ b)" non associative with precedence 45 -for @{ 'subseteq $a $b }. (* \subseteq *) - notation "hvbox(a break ∩ b)" left associative with precedence 60 for @{ 'intersects $a $b }. (* \cap *) -- 2.39.5