From e7a74589221fd564e33cb536f9c1cb43f01e028e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 13 Nov 2014 22:08:20 -0800 Subject: [PATCH] feat(library/general_notation): reserve unary minus --- library/data/int/basic.lean | 3 +-- library/general_notation.lean | 1 + 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean index de9c96ad2b..e6d4895724 100644 --- a/library/data/int/basic.lean +++ b/library/data/int/basic.lean @@ -256,8 +256,7 @@ calc definition neg : ℤ → ℤ := quotient_map quotient flip --- TODO: is this good? Note: replacing 100 by max makes it bind stronger than application. -notation `-` x:100 := neg x +notation `-` x := neg x theorem neg_comp (n m : ℕ) : -(psub (pair n m)) = psub (pair m n) := have H : ∀a, -(psub a) = psub (flip a), diff --git a/library/general_notation.lean b/library/general_notation.lean index 822f0aac71..d82767b160 100644 --- a/library/general_notation.lean +++ b/library/general_notation.lean @@ -49,6 +49,7 @@ reserve infixl `-`:65 reserve infixl `*`:70 reserve infixl `div`:70 reserve infixl `mod`:70 +reserve prefix `-`:100 reserve infix `<=`:50 reserve infix `≤`:50