Closed non closed 9 years ago
I haven't looked into the proofs for commutativity yet, I just tried to use the "canonical definitions" I'll take a crack at them tonight and see what I can do. Do you think this PR should wait on that, or would it be OK to merge now and then amend those properties later if necessary (since we would also have to change actual code in that case)?
I provided a proof of commutativity for Rng
, but I can't find one for Rig
, but also can't think of any counterexamples immediately. Nonetheless, the proof for commutativity in Rng
really hinges on an additive inverse, which doesn't exist in Rig
.
:+1: BTW
I think the bug @johnynek found is fixed, and at this point everything should be good-to-go.
Just fixed the other issues @johnynek raised. At this point my assurances don't count for much :mouse: but I think it should be good to go.
LGTM
From the main commit:
I'm not sure this is 100% good in terms of pedagogy but hopefully it is better than nothing. Maybe using the infix notation is a bad idea but I tried it with function syntax and found the laws very difficult to read and reason about.