Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] library for int32 and operation on bits

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] library for int32 and operation on bits


chronological Thread 
  • From: Frederic Blanqui <frederic.blanqui AT inria.fr>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] library for int32 and operation on bits
  • Date: Thu, 24 Mar 2011 13:36:18 +0800

You can try use the Coq library provided in http://compcert.inria.fr/ ;.

Le 24/03/2011 11:07, geng chen a écrit :
Hi, everyone

Recently, I need to define some type like int32 in C and operate the each bits of the number. For example in C, we can define bit field:
typedef struct {
    int a1         : 1;
    int a2            : 1;
    int a3              : 1;
    int a4            : 1;
    int a5             : 1;
    int a6               : 1;
    int a7            : 1;
    int a8              : 1;
    int a9               : 1;
    int a10           : 3;
    int a11   : 20;
}aa;
We can operate these fields in int32 numbers.
Can we do the same thing in Coq? Could any body give me some advise?



Archive powered by MhonArc 2.6.16.

Top of Page