diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean index ab33e4967b..c704923c1f 100644 --- a/src/Init/Notation.lean +++ b/src/Init/Notation.lean @@ -101,6 +101,7 @@ macro_rules | `($x - $y) => `(binop% HSub.hSub $x $y) macro_rules | `($x * $y) => `(binop% HMul.hMul $x $y) 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) -- declare ASCII alternatives first so that the latter Unicode unexpander wins diff --git a/tests/lean/1298.lean b/tests/lean/1298.lean new file mode 100644 index 0000000000..26c885dc49 --- /dev/null +++ b/tests/lean/1298.lean @@ -0,0 +1,15 @@ +class Semiring (R : Type u) extends Add R, HPow R Nat R, Mul R where + zero : R + +instance [Semiring R] : OfNat R n where + ofNat := Semiring.zero + +def Nat.cast [Semiring R] (n : Nat) : R := let _ := n = n; Semiring.zero + +@[defaultInstance high] instance [Semiring R] : HPow R Nat R := inferInstance + +instance [Semiring R] : CoeTail Nat R where + coe n := n.cast + +variable (R) [Semiring R] +#check (8 + 2 ^ 2 * 3 : R) = 20 diff --git a/tests/lean/1298.lean.expected.out b/tests/lean/1298.lean.expected.out new file mode 100644 index 0000000000..e7576b1e74 --- /dev/null +++ b/tests/lean/1298.lean.expected.out @@ -0,0 +1 @@ +8 + 2 ^ 2 * 3 = 20 : Prop