The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Philippe Andouard wrote:

> 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?
>  
The constructor Vcons can be used to store values in vectors.


Require Import Bvector.

About Vcons.

Implicit Arguments Vcons [A n].

Check (Vcons true (Vcons false (Vcons true (Vcons true (Vnil bool))))).

(*
Vcons true (Vcons false (Vcons true (Vcons true (Vnil bool))))
    : vector bool 4
*)



Pierre



> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>          http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>