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

[onestruggler]

This line define a semiring structure out of a boolean algebra:

agda-stdlib/src/Algebra/Lattice/Properties/BooleanAlgebra.agda

Line 170 in 8c5dee3

∧-∨-commutativeSemiring : CommutativeSemiring _ _

Here the ring multiplication * is inifxl:

agda-stdlib/src/Algebra/Bundles.agda

Line 684 in 8c5dee3

infixl 7 _*_

But here, ∧ is infixr:

agda-stdlib/src/Algebra/Lattice/Bundles.agda

Line 207 in 8c5dee3

infixr 7 _∧_

See issue #2700 (comment) 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?