[ fix #395 ] creating Data.X.Solver
#400
Conversation
| Algebra.Monoid-solver ↦ Algebra.Solver.Monoid | ||
| Algebra.CommutativeMonoidSolver ↦ Algebra.Solver.CommutativeMonoidx | ||
| Algebra.IdempotentCommutativeMonoidSolver ↦ Algebra.Solver.IdempotentCommutativeMonoid | ||
| ``` |
There was a problem hiding this comment.
Given that we went for Data.X.Categorical rather than Category.X,
wouldn't it make sense to go for Algebra.X.Solver? Or even
Algebra.Structures.X.Solver given that all of these are structures.
It would also be more consistent with the Data.X.Solver naming scheme.
There was a problem hiding this comment.
It's tricky, we're not very consistent between the "big three" (i.e. Data, Algebra and Relation). The current naming scheme is consistent within the Algebra hierarchy: Algebra.Operations.X, Algebra.Properties.X etc.
If we were to adopt your suggestion, then we should do so for all the other Algebra subfolders as well... That does seem like a big change though?
There was a problem hiding this comment.
Oh I had not realised that was the case. Better leave it as it is for the moment then!
There was a problem hiding this comment.
Yup, we'll leave it for the mythical version 2.0 😆
|
Oh one more thing I forgot I left unresolved. There's a solver in agda-stdlib/src/Function/Related/TypeIsomorphisms.agda Lines 275 to 278 in 284b407 Thoughts on |
|
Congrats on #400 btw :D |
I feel like I'm doing something wrong! There were only 50 issues in the first 10 years of the library, followed by 350 in the past 2.... |
|
No, you're just using the issue system as designed. And the number of contributors has increased, as has the size of the library. This is normal. |
|
And on the solver name - If I had my way, I would have called the whole file |
|
Added the solver file for |
Solverhierarchy, partially addressing Fix hyphenated module names #265Data.X.Propertiesto new moduleData.X.Solveraddressing Dependency cycles involving Solver modules #395Comments welcome.