coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Representation of bit sequence

From: geng chen <chengeng4001 AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Representation of bit sequence
Date: Wed, 4 Aug 2010 14:39:10 +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=hfT44rrQD8r9whp9m2IyJ5KtHj2g65dLYxbQeYYjtLidOaJ9hsQMv2XYqtmhvgQUvv 744a23qqTf/yJCzKuBid2+NrFYnY4PmlJCsbJUVdetUcISC5C7USKMHgVntZUTUQOrvu fpfXnfQAvrkTIwJbFV195MZLWiRlEa2M1NIB0=

hi, everyone
Recently, I need to represent the bit sequence in Coq and I need to transform the data into decimal number and vice versa. Is it implemented in the standard lib? I think the Bvector is not enough and hard to use.

�

Best regards,

Chen

��

[Coq-Club] Representation of bit sequence, geng chen
- Re: [Coq-Club] Representation of bit sequence, AUGER Cedric
  - Re: [Coq-Club] Representation of bit sequence, geng chen