From 28e68c7754285da0a4af5901d7cc5ed7fea9b1d7 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 3 May 2017 10:03:36 +0000 Subject: [PATCH] notation for clear --- .../basic_2/notation/relations/clear_3.ml | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/notation/relations/clear_3.ml diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/clear_3.ml b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/clear_3.ml new file mode 100644 index 000000000..09003e83a --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/clear_3.ml @@ -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( L1 ⨵ [ break term 46 f ] break term 46 L2 )" + non associative with precedence 45 + for @{ 'Clear $f $L1 $L2 }. -- 2.39.2