search

agda / agda-stdlib

The Agda standard library
https://wiki.portal.chalmers.se/agda/Libraries/StandardLibrary
Other
575 stars 237 forks source link

[fix #2253] Deprecate `Algebra.Structures.Biased.IsRing*` #2357

Closed jamesmckinna closed 5 months ago

jamesmckinna commented 5 months ago

Also: tweak v2.0 deprecation warnings (I think correctly...)

Taneb commented 5 months ago

This was added in #1684, as a migration path when the definition of IsRing was changed to not have duplicate equivalence proofs. I don't have any objection to deprecating it, but shouldn't the others added then be deprecated at the same time?

jamesmckinna commented 5 months ago

I think that the substance of the issue/PR is that zero is definable once you have _-_... and is that the case for the structures you identify? I'm not so sure that it is ...?

MatthewDaggitt commented 5 months ago

@Taneb any comment on this? I'm happy to deprecate.