[Agda] Floatpoint priorities (to wish list)

[Nils Anders Danielsson]

On 2010-06-28 14:31, Vag Vagoff wrote:
> 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?

If you read the paper you can find the motivation for our design. In
particular, we don't want to relate every operator to every other.

--
/NAD