Additions to `Data.Rational.*` about agda-stdlib HOT 3 CLOSED

I guess you could add a note to HACKING along the lines of:

Before making changes to a Data module please have a look at related modules and see if they have any content along similar lines. If so then please follow those conventions (e.g. naming, argument order). For example if working on Data.Rational, please check Data.Rational.Unnormalised or if working on Data.Vec please check Data.List and vice versa.

Feel free to edit as you seefit.

from agda-stdlib.

Err, so just to play the devil's advocate. If someone makes an addition to Data.Nat, should they also be required to make the change to Data.Nat.Binary as well?

from agda-stdlib.

Oh... hmmm. It's a good question!

I suppose I had in mind that Data.Rational.Unnormalised and Data.Rational are so tightly coupled. For whatever (blinkered) reason, I guess I view Rational as the 'abstract' interface implemented by the Unnormalised rationals?

But indeed, perhaps that's also true for your case, though my instinct suggests to me that these are some two free-standing, but nevertheless coupled, implementations of the naturals?

And of course we've also seen this many times in the List/Vec developments getting out of sync, and also within the various 'inflections' of the Vec hierarchy itself.

In any case, happy to close the issue with some sort of note in either HACKING or style-guide or do you think it's status:invalid?

from agda-stdlib.