From 75d626b7f192ab4e3495eefa5361651ba096c887 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 28 Apr 2022 14:29:08 +0200 Subject: [PATCH] update in delayed updating updated notation --- .../functions/black_downtriangle_1.ma | 4 ++-- .../functions/black_downtriangle_2.ma | 4 ++-- .../functions/black_righttriangle_1.ma | 4 ++-- .../functions/black_righttriangle_2.ma | 19 +++++++++++++++++++ 4 files changed, 25 insertions(+), 6 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/black_righttriangle_2.ma diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/black_downtriangle_1.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/black_downtriangle_1.ma index 03bfed51c..9094d139a 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/black_downtriangle_1.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/black_downtriangle_1.ma @@ -14,6 +14,6 @@ (* NOTATION FOR DELAYED UPDATING ********************************************) -notation "hvbox( ▼ term 70 t )" +notation "hvbox( ▼ term 70 p )" non associative with precedence 70 - for @{ 'BlackDownTriangle $t }. + for @{ 'BlackDownTriangle $p }. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/black_downtriangle_2.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/black_downtriangle_2.ma index f1d2a0a78..ddb2bc56d 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/black_downtriangle_2.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/black_downtriangle_2.ma @@ -14,6 +14,6 @@ (* NOTATION FOR DELAYED UPDATING ********************************************) -notation "hvbox( ▼[ term 46 t1 ] break term 70 t2 )" +notation "hvbox( ▼[ term 46 f ] break term 70 p )" non associative with precedence 70 - for @{ 'BlackDownTriangle $t1 $t2 }. + for @{ 'BlackDownTriangle $f $p }. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/black_righttriangle_1.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/black_righttriangle_1.ma index ee1a07589..93965f7e4 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/black_righttriangle_1.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/black_righttriangle_1.ma @@ -14,6 +14,6 @@ (* NOTATION FOR DELAYED UPDATING ********************************************) -notation "hvbox( ▶ term 70 t )" +notation "hvbox( ▶ term 70 p )" non associative with precedence 70 - for @{ 'BlackRightTriangle $t }. + for @{ 'BlackRightTriangle $p }. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/black_righttriangle_2.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/black_righttriangle_2.ma new file mode 100644 index 000000000..90b075806 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/black_righttriangle_2.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR DELAYED UPDATING ********************************************) + +notation "hvbox( ▶[ term 46 f ] break term 70 p )" + non associative with precedence 70 + for @{ 'BlackRightTriangle $f $p }. -- 2.39.2