From 3dae7afc87ba1c04906bd4268e2c5a9e98f72361 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Fri, 16 Sep 2005 12:13:31 +0000 Subject: [PATCH] added notation for: nleq, ngeq, nless, and ngtr --- helm/matita/core_notation.moo | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/helm/matita/core_notation.moo b/helm/matita/core_notation.moo index 38c1a4efa..c528fc111 100644 --- a/helm/matita/core_notation.moo +++ b/helm/matita/core_notation.moo @@ -30,6 +30,22 @@ notation "hvbox(a break \neq b)" non associative with precedence 45 for @{ 'neq $a $b }. +notation "hvbox(a break \nleq b)" + non associative with precedence 45 +for @{ 'nleq $a $b }. + +notation "hvbox(a break \ngeq b)" + non associative with precedence 45 +for @{ 'ngeq $a $b }. + +notation "hvbox(a break \nless b)" + non associative with precedence 45 +for @{ 'nless $a $b }. + +notation "hvbox(a break \ngtr b)" + non associative with precedence 45 +for @{ 'ngtr $a $b }. + notation "hvbox(a break + b)" left associative with precedence 50 for @{ 'plus $a $b }. -- 2.39.2