max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: use binop% for elaborating ^

Browse source 
closes #1298
This commit is contained in:
Leonardo de Moura 2022-07-12 18:20:02 -07:00
parent 95f3f6b811
commit fdef55339f
3 changed files with 17 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/Init/Notation.lean
View file

@ -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

15
tests/lean/1298.lean Normal file
View file

@ -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

1
tests/lean/1298.lean.expected.out Normal file
View file

@ -0,0 +1 @@
8 + 2 ^ 2 * 3 = 20 : Prop