The Coq mailing list

[Nikita Karetnikov <nikita AT karetnikov.org>]

“Because natural numbers are such a pervasive form of data, Coq provides
a tiny bit of built-in magic for parsing and printing them: ordinary
arabic numerals can be used as an alternative to the "unary" notation
defined by the constructors S and O.” [1]

But how exactly Coq does that?  Is it possible with a user-defined type
(e.g., binary numbers)?

[1] https://www.cis.upenn.edu/~bcpierce/sf/current/Basics.html

Attachment: pgp9Grw60BFWN.pgp
Description: PGP signature