The Coq mailing list

[geng chen <chengeng4001 AT gmail.com>]

Thanks for helping! the Compcert Coq file Integers.v is what I need. Thanks

2010/8/4 AUGER Cedric <Cedric.Auger AT lri.fr>

Le Wed, 4 Aug 2010 14:39:10 +0800,
geng chen <chengeng4001 AT gmail.com> a écrit :

> 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

Can you precise your question?

What is "the data"?
What is "decimal number"?

Post your inductive types and we can see that.

(Co?)Inductive data: Type := ...
(Co?)Inductive decimal_number: Type := ...

In coq, number types already defined are:
- nat (but it is in "base 1")
- positive (positive numbers in base 2)
- Z (negative + zero + positive in base 2)
- Real (not relying on a notion of base afaik, but I never used them)

I don't know if it is standard, but I believe we have some library of
something looking as Int32 (in fact a dependant sum with a Z and a
proof of correct range).

For data, we have a string type
(list of ascii ~ {b0:bool;b1:bool;b2:bool;...;b7:bool}; I know it is
cheating as true ascii are only 7bits).