Question about negative Integers

[Sylvain Henry]

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,
>
> 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
>