Stream: Coq users

Topic: Could I set Coq to print hexadecimal integers?


view this post on Zulip Shengyi Wang (Oct 29 2020 at 10:33):

Since 8.12.0, Coq supports parsing hexadecimal numbers in the form starting with "0x" such as 0x39A7F8. When I Check 0x39A7F8, Coq gives its decimal form 3778552: Z. I'm curious is there any settings to print decimal integers in hexadecimal form? I know there are functions to convert between hexadecimal and decimal strings. I ask for literal forms, not strings. Thank you.

view this post on Zulip Pierre Roux (Nov 05 2020 at 10:43):

Sorry for the late answer, for nat you can

view this post on Zulip Pierre Roux (Nov 05 2020 at 10:43):

Open Scope hex_nat_scope.

view this post on Zulip Pierre Roux (Nov 05 2020 at 10:43):

Coq < Check 0xa.
0xa
     : nat

view this post on Zulip Pierre Roux (Nov 05 2020 at 10:44):

But there is currently no hexadecimal printer provided for Z.

view this post on Zulip Pierre Roux (Nov 05 2020 at 10:53):

You could probably rather easily develop one taking inspiration from
https://github.com/coq/coq/blob/5af74f736d5d621e3934be17d25c69b4ed3c0edf/theories/Init/Prelude.v#L52
https://github.com/coq/coq/blob/5af74f736d5d621e3934be17d25c69b4ed3c0edf/theories/Init/Nat.v#L241
https://github.com/coq/coq/blob/5af74f736d5d621e3934be17d25c69b4ed3c0edf/theories/ZArith/BinIntDef.v#L671

view this post on Zulip Pierre Roux (Nov 05 2020 at 10:54):

If you do so, a pull request would be welcome to integrate it into the standard library.

view this post on Zulip Paolo Giarrusso (Nov 05 2020 at 17:50):

along the way, you’ll probably need a printer for positive, and then one for N should be close by (given definitions in coq/theories/Numbers/BinNums.v)

view this post on Zulip Shengyi Wang (Jan 15 2021 at 03:36):

Thank you both very much!

view this post on Zulip Pierre Roux (May 17 2021 at 08:03):

@Shengyi Wang FYI, hex_{Z,N,positive}_scopeare now available in Coq master, hence will be in the upcoming 8.14: https://github.com/coq/coq/pull/14263


Last updated: Jan 29 2023 at 06:02 UTC