Description
The macro for the ^ notation for exponentiation is defined as
macro_rules | `($x ^ $y) => `(binop% HPow.hPow $x $y)
However, the binop% elaborator tries to make the type of x and y the same, which is not desired for exponentiation.
MWE
class NatCast (R : Type u) where
natCast : Nat → R
instance [NatCast R] : CoeTail Nat R where coe := NatCast.natCast
instance [NatCast R] : CoeHTCT Nat R where coe := NatCast.natCast
axiom Real : Type
notation "ℝ" => Real
instance (n : Nat) : OfNat ℝ n := sorry
variable (a : ℝ)
instance natCast : NatCast ℝ where natCast n := sorry
instance : HPow ℝ Nat ℝ := sorry
set_option pp.all true
#check a ^ 4
-- @HPow.hPow.{0, 0, 0} Real Nat Real instHPowRealNat a (@OfNat.ofNat.{0} Nat 4 (instOfNatNat 4)) : Real
instance : HPow ℝ ℝ ℝ := sorry
#check a ^ 4
-- @HPow.hPow.{0, 0, 0} Real Real Real instHPowReal a (@OfNat.ofNat.{0} Real 4 (instOfNatReal 4)) : Real
#check a ^ (4 : Nat)
-- @HPow.hPow.{0, 0, 0} Real Real Real instHPowReal a (@NatCast.natCast.{0} Real natCast (@OfNat.ofNat.{0} Nat 4 (instOfNatNat 4))) : RealThe desired result is that all checks use the instHPowRealNat instance, i.e. that 4 is interpreted as a Nat.
Additional Notes
Just removing binop% and replacing the macro with the following fixes the current issue, but it causes problems in other elaboration problems.
macro_rules | `($x ^ $y) => `(HPow.hPow $x $y)
With this macro an example like the following fails.
example (n : Nat) := ∃ k, n = 2 ^ k -- fails to find any instance, needs to know the type of `k`
Zulip Discussion
link
Description
The macro for the
^notation for exponentiation is defined asHowever, the
binop%elaborator tries to make the type ofxandythe same, which is not desired for exponentiation.MWE
The desired result is that all checks use the
instHPowRealNatinstance, i.e. that4is interpreted as aNat.Additional Notes
Just removing
binop%and replacing the macro with the following fixes the current issue, but it causes problems in other elaboration problems.With this macro an example like the following fails.
Zulip Discussion
link