Agda-stdlib: Set the fixity of mixfix definitions

[MatthewDaggitt]

Set the fixity of _

[MatthewDaggitt]

Closed with 5f4c67eca643120a275bea894716c76cc9f2defc

[gallais]

Using the new -Wall option which I have just introduced, I have
found a lot more mixfix definitions which do not come with a fixity
declaration:

https://gist.github.com/gallais/79386a6ba8826620dc82b3f5d5af2bde

[andreasabel]

Well, bracketing constructs like [_] or [_,_] do not need a fixity, in fact, since they are neither pre/post nor infix operators, a precedence or associativity value for these does not make sense.
The warning mechanism should be adapted to disregard these.

[gallais]

I've updated the gist with the new set of warnings ignoring well-bracketed mixfix decls

[MatthewDaggitt]

As of Agda 2.6.0 the warnings for the missing fixities should now work properly, so this should be much more doable.

[MatthewDaggitt]

Particularly egregious example in Relation.Binary.Construct.NonStrictToStrict

[JacquesCarette]

@gallais can you update the gist please? I think I'm going to spend some of my time working on this.

[gallais]

@JacquesCarette It's just a matter of running agda on Everything with -Wall.