From c4ee4f93850d64a1ad583c0fa00a4c38d2c43a88 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 3 May 2017 10:12:43 +0000 Subject: [PATCH] more notation for s-steps --- .../basic_2/notation/relations/supterm_7.ma | 19 +++++++++++++++++++ .../notation/relations/suptermopt_7.ma | 19 +++++++++++++++++++ .../notation/relations/suptermplus_7.ma | 19 +++++++++++++++++++ .../notation/relations/suptermstar_7.ma | 19 +++++++++++++++++++ 4 files changed, 76 insertions(+) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/notation/relations/supterm_7.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/notation/relations/suptermopt_7.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/notation/relations/suptermplus_7.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/notation/relations/suptermstar_7.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/supterm_7.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/supterm_7.ma new file mode 100644 index 000000000..a312023d1 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/supterm_7.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 THE FORMAL SYSTEM λδ ****************************************) + +notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ⊐ [ break term 46 b ] ⦃ break term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )" + non associative with precedence 45 + for @{ 'SupTerm $b $G1 $L1 $T1 $G2 $L2 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/suptermopt_7.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/suptermopt_7.ma new file mode 100644 index 000000000..307ecd3a5 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/suptermopt_7.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 THE FORMAL SYSTEM λδ ****************************************) + +notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ⊐⸮ [ break term 46 b ] ⦃ break term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )" + non associative with precedence 45 + for @{ 'SupTermOpt $b $G1 $L1 $T1 $G2 $L2 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/suptermplus_7.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/suptermplus_7.ma new file mode 100644 index 000000000..83b76de13 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/suptermplus_7.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 THE FORMAL SYSTEM λδ ****************************************) + +notation "hvbox( ⦃ term 46 G1, term 46 L1, break term 46 T1 ⦄ ⊐ + [ break term 46 b ] ⦃ break term 46 G2, term 46 L2 , break term 46 T2 ⦄ )" + non associative with precedence 45 + for @{ 'SupTermPlus $b $G1 $L1 $T1 $G2 $L2 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/suptermstar_7.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/suptermstar_7.ma new file mode 100644 index 000000000..db96fc7e9 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/suptermstar_7.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 THE FORMAL SYSTEM λδ ****************************************) + +notation "hvbox( ⦃ term 46 G1, term 46 L1, break term 46 T1 ⦄ ⊐ * [ break term 46 b ] ⦃ break term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )" + non associative with precedence 45 + for @{ 'SupTermStar $b $G1 $L1 $T1 $G2 $L2 $T2 }. -- 2.39.2