feat: use unop% to implement unary minus notation

closes #1779

src/Init/Notation.lean

@@ -280,6 +280,7 @@ macro_rules | `($x / $y)   => `(binop% HDiv.hDiv $x $y)
 macro_rules | `($x % $y)   => `(binop% HMod.hMod $x $y)
 macro_rules | `($x ^ $y)   => `(binop% HPow.hPow $x $y)
 macro_rules | `($x ++ $y)  => `(binop% HAppend.hAppend $x $y)
+macro_rules | `(- $x)      => `(unop% Neg.neg $x)
 
 -- declare ASCII alternatives first so that the latter Unicode unexpander wins
 @[inherit_doc] infix:50 " <= " => LE.le

tests/lean/1779.lean

@@ -0,0 +1,27 @@
+section
+variable [Coe Int R] [Neg R] (a : R) (n : Int)
+#check a = -n
+#check a = (-n : R)
+#check -n = a
+#check (-n : R) = a
+end
+
+section
+variable [Coe Int R] [Add R] (a : R) (n : Int)
+#check a = n + n
+#check a = (n + n : R)
+end
+
+section
+variable [Coe Int R] [OfNat R 0] [Sub R] (a : R) (n : Int)
+#check a = 0 - n
+#check a = (0 - n : R)
+end
+
+section
+variable [Coe Int R] [Add R] [Neg R] (a : R) (n : Int)
+#check a + -n
+#check a + (-n : R)
+#check -n + a
+#check (-n : R) + a
+end

tests/lean/1779.lean.expected.out

@@ -0,0 +1,12 @@
+a = -Coe.coe n : Prop
+a = -Coe.coe n : Prop
+-Coe.coe n = a : Prop
+-Coe.coe n = a : Prop
+a = Coe.coe n + Coe.coe n : Prop
+a = Coe.coe n + Coe.coe n : Prop
+a = 0 - Coe.coe n : Prop
+a = 0 - Coe.coe n : Prop
+a + -Coe.coe n : R
+a + -Coe.coe n : R
+-Coe.coe n + a : R
+-Coe.coe n + a : R