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.

Sorry for the late answer, for nat you can

`Open Scope hex_nat_scope.`

```
Coq < Check 0xa.
0xa
: nat
```

But there is currently no hexadecimal printer provided for `Z`

.

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

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

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)

Thank you both very much!

@Shengyi Wang FYI, `hex_{Z,N,positive}_scope`

are now available in Coq master, hence will be in the upcoming 8.14: https://github.com/coq/coq/pull/14263

Last updated: Jun 18 2024 at 22:01 UTC