change of ^

Stream: general

[Kevin Buzzard]

Are there any general tips for how to fix up files which no longer compile because of changes to ^? I have files which start local infix ` ^ ` := monoid.pow, and for x and y in a comm_semiring (x + y) ^ 0 = x ^ 0 * y ^ 0 used to be solved by simp and now does not seem to be.

[Kevin Buzzard]

I should say that I'm looking at @Chris Hughes 's code here so I might not have got this 100 percent right

[Kevin Buzzard]

but basically our stacks project is quite broken now I upgraded to the current nightly

[Chris Hughes]

simp [pow_succ, pow_zero]?