infixity mismatch between `_∧_` and the ring multiplication `_*_`

[onestruggler]

This line define a semiring structure out of a boolean algebra: https://github.com/agda/agda-stdlib/blob/8c5dee34ebde4734f8da5369c3f735576a6311fc/src/Algebra/Lattice/Properties/BooleanAlgebra.agda#L170

Here the ring multiplication * is inifxl:

https://github.com/agda/agda-stdlib/blob/8c5dee34ebde4734f8da5369c3f735576a6311fc/src/Algebra/Bundles.agda#L684

But here, ∧ is infixr:

https://github.com/agda/agda-stdlib/blob/8c5dee34ebde4734f8da5369c3f735576a6311fc/src/Algebra/Lattice/Bundles.agda#L207

See issue https://github.com/agda/agda-stdlib/issues/2700#issuecomment-2804408528 for an example for the inconvenience rooting to this problem.

[jamesmckinna]

Good spot... that's a deep cut. Presumably also for infixr 6 _∨_ and infixl 6 _+_?

Not clear what the best resolution strategy might be however? Whatever, it will probably end up being breaking?

[JacquesCarette]

Is this so deep that it is in the style-guide for fixities?

[jamesmckinna]

Is this so deep that it is in the style-guide for fixities?

Sadly, the style-guide does indeed seem to reify the distinction https://github.com/agda/agda-stdlib/blob/0fa3e60393bed7cb1c5a377b646659c0e951be4b/doc/style-guide.md?plain=1#L606-L608 and https://github.com/agda/agda-stdlib/blob/0fa3e60393bed7cb1c5a377b646659c0e951be4b/doc/style-guide.md?plain=1#L614-L616.

[JacquesCarette]

Changing that would likely break code. (Not the style-guide but the actual inconsistency.) v3.0 candidate?