Fix #2396 by removing redundant zero in IsNonAssociativeRing

agda / agda-stdlib

The Agda standard library

https://wiki.portal.chalmers.se/agda/Libraries/StandardLibrary

Other

561 stars 234 forks source link

Fix #2396 by removing redundant zero in IsNonAssociativeRing #2410

Open lexvanderstoep opened 2 weeks ago

lexvanderstoep commented 2 weeks ago

The zero field in the IsNonAssociativeRing was redundant, and could be replaced with a proof based on the other properties.

jamesmckinna commented 2 weeks ago

Thanks for the speedy follow-up on the issue... but the failing CI tests show that replacing the (redundant) explicit field with a definition/manifest field is breaking behaviour... so we need to tread a bit more carefully!

Issues:

knock-on consequences: need to update uses/definitions to accommodate the change
breaking changes are generally being punted to v3.0, rather than any v2.x minor version
needs CHANGELOG (But in view of the version issue, this can, and probably should, wait for the time being...)

lexvanderstoep commented 2 weeks ago

Thanks for reviewing this so quickly! I was about to mark the PR as a draft to fix the usage of IsNonAssociativeRing, but you beat me to it.

About the change being breaking and only included in v3.0, makes sense. What is the way forward? Do we leave the MR until we're ready to release the next major version of the library?

jamesmckinna commented 2 weeks ago

I'd definitely go with DRAFT for the time being... I could well imagine some of the other maintainers weighing in on how best to take this forward... and when. But we're a bit more focused on clearing the v2.1 milestone, so this one will definitely be on the back burner for a bit, I think.

lexvanderstoep commented 2 weeks ago

Sounds like a plan!