coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] Coq library for hexadecimal?, 朱立平, 01/25/2019
- Re: [Coq-Club] Coq library for hexadecimal?, Xavier Leroy, 01/25/2019
- Re: [Coq-Club] Coq library for hexadecimal?, Gaëtan Gilbert, 01/25/2019
- Re: [Coq-Club] Coq library for hexadecimal?, Xavier Leroy, 01/25/2019
Archive powered by MHonArc 2.6.18.