How to force use of natural powers

Stream: new members

[Richard Hill]

I have a very silly question. I'd like an easy way of stating (for example) that 1^2 = 1, where 1 is the real number and 2 is a natural number. If I don't import very much, then I can simply type

import Mathlib.Tactic
example : (1 : ℝ)^2 = 1 := sorry

However, if I import Mathlib, then the same code would be interpreted as raising 1 to the power of the
real number 2. The only way around this that I know is

import Mathlib
example : @HPow.hPow ℝ ℕ ℝ _ 1 2 = 1 := sorry

What is the right way to do this?

[Eric Wieser]

The fact this is annoying is a bug, lean4#2220

[Eric Wieser]

The workaround is

macro_rules | `($x ^ $y)   => `(HPow.hPow $x $y)

[Eric Wieser]

Can we just commit this to Mathlib already while we wait for an upstream patch?

[Richard Hill]

Thank you!