16 Nov
2019
16 Nov
'19
11:04 a.m.
Hi, Am Freitag, den 15.11.2019, 17:04 +0100 schrieb Sylvain Henry:
However integer-gmp and integer-simple fake two's complement encoding for Bits operations.
just a small factoid: the Coq standard library provide the same semantics. I’d lean towards leaving it as it is. If someone need the “other” semantics, they can easily throw in a (very efficient) `abs` in the right places. Cheers, Joachim -- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/