[Agda] Floatpoint priorities (to wish list)

[Vag Vagoff]

> We have plans to switch to more descriptive fixity declarations, but
> have not gotten around to it yet. See "Parsing Mixfix Operators" for
> more details:

Perhaps floatpoint priorities appeared to be disgusting for mathematician because
it uses redundant concept (while mathematicians like to abstract out things) that
is not derived naturally from primary task: floating point weight.
But I ponder that floatpoint priorities will be less error prone due to
inability of accidentally forgetting required relation to some other operation.
Am I correct?