16 Nov
2019
16 Nov
'19
12:30 p.m.
Alright. Thanks everyone for the convincing answers. I will keep the current behavior and I will document that operations may be slower than could be expected. Cheers, Sylvain On 16/11/2019 12:04, Joachim Breitner wrote:
Hi,
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
Am Freitag, den 15.11.2019, 17:04 +0100 schrieb Sylvain Henry: the right places.
Cheers, Joachim