coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Coq library for hexadecimal?

From: 朱立平 <zlponline AT 163.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Coq library for hexadecimal?
Date: Fri, 25 Jan 2019 17:57:37 +0800 (CST)
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=zlponline AT 163.com; spf=Pass smtp.mailfrom=zlponline AT 163.com; spf=None smtp.helo=postmaster AT m13-62.163.com
Ironport-phdr: 9a23:soGW7xUQUE7x6YWTLsBI87tlrifV8LGtZVwlr6E/grcLSJyIuqrYYxSBt8tkgFKBZ4jH8fUM07OQ7/iwHzRYqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba9xIRmssQndqtQdjJd/JKo21hbHuGZDdf5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2UbJXDDI9M2Ao/8LrrgXMTRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5KptVRTmijoINyQh/WHWhMJ+jLxVrg+7qRJ434Hbb4KbOeFkca/BZ94VXnBMUtpNWSFHH4iyb5EPD+0EPetAt4/6ul8LrhynAAysGejizT5Jhnvu3a091eQhFQDG3Ao+EN8VrXjZrdv4OL0OXuCyyanF1DPOZO5Y1zf67YjHaBEhofeUULJxd8rR00gvGBnfglWes4zoOS6e2OcVs2WD8eZsS/6jh3Q6pwxyvzSj3Nogh4fTio8U1FzI7Th1zJsoKdGiVUJ2ZcSoHZVTui2AKYd6X8wvTmd1sygg0LIGo4S0fC0SxZQn2RHfb/uHfpCN4h7+WuudODZ1iGx/dL6ihhu//1KsxfH7VsmxyFpKryxFncfQtn0VyRDf9NSLRuFg8kqixDqDzR3f5+9eLU01i6bXM5shzaQxlpoXv0TDBCj2mEDuga6XckUk4u+o6+LjYrXnoJ+TKZR5hhz/P6kggMCwHeM4Mg0WU2iB5eu8zKHj/VH+QLhSkvI2lbDZvInGKsQfu662GBRY0p0j6ha6Fzepys4UnXgBLFJfeRKIlZLlO1/UIKOwMfDqiFO11Txv2vruP7v7A5yLIGKQvq3meOPDb+eWZt97mcJb/5VSDrAHLdqqBBS3v9vdWExqezeoyvrqXY0unrgVXniCV/fAYfHi9GSQ7+dqGNGiIYocuTLzMf8gtqy30yR/klgYL/DwgcknLUugF/EjGH23JGL2i4ZTSDlR+AE5Sb6y0QDQYXtof3+3GpkEyHQ7BYahVNmRQ9n2xeLbmn7lRdtdYWUUUl0=

Could anyone give some library suggestion on hex numbers? I see https://coq.inria.fr/library/Coq.Strings.HexString.html but it lack function like hex to int.

More precisely, I'm using Integers library from CompCert, and I want to replace Int.repr 65535 to some constructor and a parameter 0xFFFF.

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