Shengyi Wang (Oct 29 2020 at 10:33): 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.
Pierre Roux (Nov 05 2020 at 10:43):Sorry for the late answer, for nat you can
Pierre Roux (Nov 05 2020 at 10:43):Open Scope hex_nat_scope.
Pierre Roux (Nov 05 2020 at 10:43):Coq < Check 0xa.
0xa
: nat
But there is currently no hexadecimal printer provided for Z.
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
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.
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)
Shengyi Wang (Jan 15 2021 at 03:36):Thank you both very much!
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: Oct 04 2023 at 20:01 UTC