coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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?
- [Coq-Club] library for int32 and operation on bits, geng chen
- Re: [Coq-Club] library for int32 and operation on bits, Frederic Blanqui
- Re: [Coq-Club] library for int32 and operation on bits,
AUGER Cedric
- Re: [Coq-Club] library for int32 and operation on bits, Sandrine Blazy
Archive powered by MhonArc 2.6.16.