The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

> However it looks like it's not compiled and installed by default in Coq
> 8.8.2.   Am I the only one who cannot "Require Import
> Coq.Strings.HexString" ?

HexString is new to 8.9, see changes "There are now conversions between 
`string` and `positive`, `Z`, `nat`, and `N` in binary, octal, and hex."



Gaëtan Gilbert

On 25/01/2019 11:59, Xavier Leroy wrote:
> On Fri, Jan 25, 2019 at 10:59 AM 朱立平 <zlponline AT 163.com 
> <mailto:zlponline AT 163.com>> wrote:
>
>     Could anyone give some  library suggestion  on hex numbers? I see
>     https://coq.inria.fr/library/Coq.Strings.HexString.html 
>
>
> I didn't know about this library module, and it looks nice. Thanks for 
> mentioning it!
>
> However it looks like it's not compiled and installed by default in Coq 
> 8.8.2.   Am I the only one who cannot "Require Import 
> Coq.Strings.HexString" ?
>
>     but it lack function like hex to int.
>
>
> Really? See function "to_Z".
>
>     More precisely, I'm using /Integers /library from CompCert, and I
>     want to replace /Int.repr 65535 /to  some constructor and a
>     parameter /0xFFFF/.
>
>
> Definition someconstructor (s: string) : int :=
>     Int.repr (HexString.to_Z s).
>
> Kind regards,
>
> - Xavier Leroy
>
>
>
>     Best regards,
>     Julian