Zulip Chat Archive

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: Dec 20 2023 at 11:08 UTC