agda
lib-2.0: factors-∣ rather than ∣-factors in divisibility in CommutativeMagma
lib-2.0 has in Algebra.Properties.CommutativeMagma.Divisibility:
∣-factors : ∀ x y → (x ∣ x ∙ y) × (y ∣ x ∙ y)
This means "each of factors divides the product".
But seeing the name only, the user would think "something divides each of factors".
Therefore the name rather has to be factors-∣
Has it?
The same is with ∣-factors-≈
I agree that this would be pronounced "factors divide" and so a name that puts things in the same order makes sense.
The naming convention of the standard library is either to spell out the type explicitly, or put the operator at the front of "meaningful" word. So factors-∣ would not be in line with that.
We could rename it x|xy∧y|xy?
May be, change this convention?
On the other hand x|xy∧y|xy looks reasonable.
May be, change this convention?
I don't think the chaos and the ~200 people hours that would involve is really worth it...