coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: geng chen <chengeng4001 AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] library for int32 and operation on bits
Date: Thu, 24 Mar 2011 11:07:51 +0800
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:date:message-id:subject:from:to:content-type; b=bWIEtgAMx1XRoJcoAFkgSbwwcoIHhVfEs4aIuo9WszRb4bcg7mdDG2u8Nxgmt4wd5I uGG/f3ACjmeTcIyOB+Y6+PTx0CMOTqhyWOg8mWEv9J/0NuSJF2yc9TIrabpUEi5wUg0L JtOFqXjI5hF1++Nl6bk4w37CyUbppxYLU67IY=

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