negative squares

Stream: lean4

[Alex J. Best]

Way back in May 2020 we changed the precedence of unary negation to be lower than the power operator in the community edition of lean 3 lean#287 (following https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Negative.20squares/near/197021708).
In Lean 4 it seems that the defaults are the same as in Lean 3.4.2, so that Lean 4 and Lean 3 community now behave differently when taking (even) powers of negative numbers (eg. integers, floats,...):

--Lean 4
#eval -(1:Int)^2 --     1

-- community lean 3
import data.int.basic
#eval -(1:ℤ)^2 --     -1

Was this an intentional choice for Lean 4?
If not (or even if so) is there support for changing this in Lean 4 so that -1^2 = -1.
The motivation is the same as in the thread linked above, this is a less surprising convention mathematically and to users of computer algebra systems this can be a source of copy-paste inconsistencies when moving things to lean.

[Kevin Buzzard]

The precedence of Boolean not ! has also changed leading to issues when I was porting data.bool.basic

[Sebastian Ullrich]

Was this an intentional choice for Lean 4?

Recall that Lean 4 has been forked from Lean 3.3.0 :) . So the most probable default answer is "no-one has proposed the corresponding change for Lean 4 so far". If the motivation applies to Lean 4 just as well, I'd say go ahead and PR it.