diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean index de9c96ad2..e6d489572 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 822f0aac7..d82767b16 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