Topic: ring to semiring
Chris Hughes (Jul 15 2019 at 08:27):
I changed the assumption on one theorem from
semiring, and now
simp won't use that theorem on rationals. Will this be fixed? It makes code very sensitive to minor changes.
Kenny Lau (Jul 15 2019 at 08:50):
do you have a MWE?
Chris Hughes (Jul 15 2019 at 08:59):
It's actually more obvious what's going on after making the MWE. Changing the assumption from
mul_right_eq_of_mul_eq fixes the problem
Kenny Lau (Jul 15 2019 at 09:01):
glad you fixed it then
Chris Hughes (Jul 15 2019 at 09:02):
Not a long term fix. What if
mul_right_eq_of_mul_eq hadn't been true in a
Last updated: May 10 2021 at 07:15 UTC