I broke the tests

Stream: general

[Kevin Buzzard]

In an attempt to get #3716 up and running again, I made an irred-with-zero branch of mathlib, which makes with_zero and with_one irreducible. I was surprised how little of mathlib broke with this: I only had to edit 7 files. Continuous integration threw up a shock though -- mathlib built and linted fine, but I broke the tests. What do I do now?

[Kevin Buzzard]

On further investigation, I claim that the tests have a bug in. This line here is incorrect. The definition of with_zero in the hidden namespace on line 60 is the one being used here; the has_zero instance defined on line 66 will be, as @Mario Carneiro can confirm, called hidden.has_zero, and so line 74 is abusing the fact that hidden.with_zero = with_zero. Is this what the test is supposed to be testing? Can I "fix" this test?

[Mario Carneiro]

I would guess that you should change it to say hidden.with_zero.has_zero

[Mario Carneiro]

after making the instance name be that

[Kevin Buzzard]

#3859 I just went with the Lean naming conventions :-/

[Johan Commelin]

@Kevin Buzzard I kicked it on the queue