Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Coq library for hexadecimal?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Coq library for hexadecimal?


Chronological Thread 
  • From: Xavier Leroy <xavier.leroy AT college-de-france.fr>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Coq library for hexadecimal?
  • Date: Fri, 25 Jan 2019 11:59:41 +0100
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=xavier.leroy AT college-de-france.fr; spf=Pass smtp.mailfrom=xavier.leroy AT college-de-france.fr; spf=None smtp.helo=postmaster AT smtpout10.partage.renater.fr

On Fri, Jan 25, 2019 at 10:59 AM 朱立平 <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




 




Archive powered by MHonArc 2.6.18.

Top of Page