diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean index ccaffbffc6..8c492826ee 100644 --- a/src/Init/Notation.lean +++ b/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 diff --git a/tests/lean/1779.lean b/tests/lean/1779.lean new file mode 100644 index 0000000000..bf50190356 --- /dev/null +++ b/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 diff --git a/tests/lean/1779.lean.expected.out b/tests/lean/1779.lean.expected.out new file mode 100644 index 0000000000..5bed378223 --- /dev/null +++ b/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