coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club][Bvector]

From: "Philippe Andouard" <phil.andouard AT gmail.com>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club][Bvector]
Date: Tue, 25 Apr 2006 09:51:49 +0200
Domainkey-signature: a=rsa-sha1; q=dns; c=nofws; s=beta; d=gmail.com; h=received:message-id:date:from:to:subject:mime-version:content-type:content-transfer-encoding:content-disposition; b=hau4tgkMmjHLkU0/kvMUO5dwncOdOum5s/dLFdAl3gtD0K3gXZ01hji7xHOXBlAHfjHFBSuihZ7gQmgn9q/KWoWWcriuH6mqstVA7krOp57WUCOkiYZfSZOoSZdLVZG67QjfIG/IHnWSTeOC5Jd57p1v/XDl0PT6gxQagNHMO/o=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Bonjour,

J'aimerais pouvoir simuler le fonctionnement d'un octet. J'ai vu que
la librairie standard de Coq proposait des vecteurs de bits au travers
du module Bvector.

Mon probl�me est le suivant, je voudrais convertir un entier en base
dix en sa repr�sentation en base deux et le stocker dans un vecteur de
bits. Par exemple si on consid�re l'entier 15 je voudrais pouvoir
stoker [0 0 0 0 1 1 1 1] dans mon vecteur.
J'arrive � d�clarer des Bvector mais je n'arrive pas � stocker quoi
que ce soit dedans.

Quelqu'un saurait-il comment stocker des valeurs dans des vecteurs?

[Coq-Club][Bvector], Philippe Andouard
- Re: [Coq-Club][Bvector], Pierre Casteran
  - Re: [Coq-Club][Bvector] + NArith + Intmap ..., Pierre Letouzey