raffopazzo / depc

Like C and C++ but with Dependent Types
1 stars 1 forks source link

wrong precedence between {xor, and, or} #61

Closed raffopazzo closed 5 days ago

raffopazzo commented 1 month ago

The three operators appear to have the wrong precedence when compared to C++, cf:

Admittedly, C++ does not define a logical xor operator so the comparison is really against C++ bitwise operator but it's essentially the same thing.

raffopazzo commented 6 days ago

C++ is a bit insane... a xor b and c actually translates to a ^ b && c thereby mixing together bitwise-xor with logical-and which yields a different result from a ^ b & c (!) where both operations are bitwise...

raffopazzo commented 5 days ago

It needs to be noted that a xor b is equivalent to a != b. With this in mind, one could argue that it can be somewhat useful to have the xor operator with the new precedence since the expressions a != b and c is parsed differently to a xor b and c, namely (a != b) and c for the former and a xor (b and c) for the latter. But prelude defines lemmas for != with respect to bool which would need to be duplicated for xor at which point the added benefit of xor becomes relatively expensive when instead one can just add parenthesis and write a != (b and c) for the second example. In conclusion, it's better to remove xor altogether!