RFC for fixing lean4#2220

Stream: lean4

[Kyle Miller]

I'd like to mention RFC lean4#2854 to fix the elaboration issues with ^ that we experience in mathlib. There is also a PR that implements the changes (lean4#2778) and with it we can remove the local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) workaround that turns off binop% from mathlib.

This is technically a breaking change, but testing suggests that ^ for Nat and Float end up elaborating the same as before. The std library does not need any modification.

[Kyle Miller]

If you have a project that depends on the finer details of how ^ elaborates, it would be good to hear your input!

There is a pre-built Lean toolchain if you want to test it out: leanprover/lean4-pr-releases:pr-release-2778

If you are using mathlib, you can try the mathlib branch lean-pr-testing-2778, which also includes a large-scale test of hooking SMul into this elaborator. For a mathlib version bump, we might or might not include this SMul adjustment depending on community input.

[Scott Morrison]

This is fantastic news!