Comments (3)
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 onData.Rational
, please checkData.Rational.Unnormalised
or if working onData.Vec
please checkData.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.
Related Issues (20)
- [DRY] Refactor `Algebra.Solver.*Monoid` (or deprecate entirely?)
- Rename `WeaklyDecidable`? HOT 4
- Add `Algebra.Properties.IdempotentCommutativeMonoid`
- Naming of new functions `tail∘inits` and `tail∘tails` HOT 5
- comments on lib-2.1 candidate 1 HOT 9
- Unify general algebraic definitions of Divisibility and Primarity with those in Nat and Integer HOT 7
- Style for lower/upper case for initial letter in denotations HOT 7
- Restore missing proofs from `Algebra.Operations.CommutativeMonoid`
- Proofs in `Data.Vec.Properties` take general properties as inputs HOT 23
- Unsolved metas in `Data.List.Properties` cf. discussion on #2415, #2359, #2365 HOT 3
- [DRY] Refactor the various definitions of 'pointwise' equality on functions/`Function`s/pointwise `Algebra`s HOT 2
- Data.Nat.Properties.≤-total should be implemented with _<ᵇ_ HOT 14
- Data.List.upTo/applyUpTo can be made faster HOT 5
- Linear-time implementation of `Data.Nat.Properties.≤′⇒≤`? HOT 3
- Regression in the documentation of installation HOT 1
- Refactor ` Data.Nat.GeneralisedArithmetic` HOT 2
- Derived operators in the theory of `Relation.Binary.Structures.IsTotalOrder` HOT 5
- Deploy doc rendering for v2.1 HOT 2
- Add `Algebra.Definitions.RawGroup` and `Algebra.Properties.Group.*`
- Get rid of inconsistent `homo` name in algebra hierarchy?
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from agda-stdlib.