Question about negative Integers

[Joachim Breitner]

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 at joachim-breitner.de
  http://www.joachim-breitner.de/