Ring law is unclear

[hdgarrood]

We currently have:

Additive inverse: a + (-a) = (-a) + a = zero

However, this is a little unclear, since there is no unary prefix (-) available. I think we should do one of the following:

• Swap sub and negate around, so that negate is part of Ring, and (-) is defined as x - y = x + negate y.
• Reformulate the additive inverse law in terms of binary (-), for example: a - a = (zero - a) + a = zero?

[garyb]

The parser has a special case for -a, it desugars to negate a.

[hdgarrood]

ha, silly me, I should have checked first. Do you think it should be left alone then?

[garyb]

I don't mind either way actually... @paf31? :)

[michaelficarra]

I like both. They are both better than what we have now.

[paf31]

Either way is fine with me 👍