The Coq mailing list

[Sandrine Blazy <Sandrine.Blazy AT irisa.fr>]

Le 24/03/11 10:31, AUGER Cedric a écrit :
> Le Thu, 24 Mar 2011 11:07:51 +0800,
> geng 
> chen<chengeng4001 AT gmail.com>
>   a écrit :
> To sum up, I advise you to take a look on the compcert project,
> they have a good set of operations on integers, sorry I don't send you
> a link, but I can't find the online documentation of compcert (I was
> pretty sure there was one, but I don't find it).
The link to the representation of 32-bits machine integers in CompCert is
http://compcert.inria.fr/doc/html/Integers.html

This representation relies on Coq arbitrary-precision integers (type
Z). Bitwise operations are defined on these integers using a
conversion between Coq integers Z and their bit-level representations.