## Stream: general

### Topic: change of ^

#### Kevin Buzzard (Apr 06 2018 at 12:39):

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 (Apr 06 2018 at 12:39):

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 (Apr 06 2018 at 12:40):

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

#### Chris Hughes (Apr 06 2018 at 13:37):

simp [pow_succ, pow_zero]?

Last updated: May 10 2021 at 23:11 UTC