The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

On 10/11/2014 07:03 PM, Nikita Karetnikov wrote:
> But how exactly Coq does that?
It has been implemented as a plugin written in OCaml, see

  plugins/syntax/nat_syntax.ml

in the Coq source tree.

> Is it possible with a user-defined type (e.g., binary numbers)?
Yes, but not in a nice modular way. You can just copy/paste the file 
mentioned above, and make it work with your own number type.

However, for the binary naturals (the types positive, N, and Z) from the 
standard library, Coq already has built in syntax support in the same 
way as for nat.