The Coq mailing list

[Eddy Westbrook <westbrook AT galois.com>]

Sorry for the delayed response, but thanks for the pointer, that looks very 
helpful!

-Eddy

> On Jan 13, 2018, at 8:09 AM, Xavier Leroy 
> <Xavier.Leroy AT inria.fr>
>  wrote:
> 
> On 01/12/2018 11:32 PM, Eddy Westbrook wrote:
> 
>> Is there already a type of 64-bit integers in the Coq standard library? Or 
>> at least 32-bit integers? I see some evidence of these in the 
>> documentation of some of the numeric modules, but I don’t really 
>> understand them…
> 
> Maybe you stumbled on the 31-bit machine integers that are used in one of 
> the implementations of (mathematical, arbitrary-precision) integers from 
> Coq's standard library.  But those 31-bit integers are not really usable on 
> their own.
> 
> For N-bit integer arithmetic in the style of C or Java, you could use 
> CompCert's "Integers" library,
>   http://compcert.inria.fr/doc/html/Integers.html  
> It defines (as a parameterized module) N-bit integers and their signed and 
> unsigned arithmetic and logical operations, plus a whole lot of theorems 
> about those operations.  Instantiations for N=8, N=32 and N=64 are 
> provided, with extra operations and theorems relating 32- and 64-bit 
> integers.
> 
> - Xavier Leroy