The Coq mailing list

[Arthur Azevedo de Amorim <arthur.aa AT gmail.com>]

Another thing you can do is to write your own parser for your notation
in Coq itself and use Coq strings to fake a "real" notation, e.g.
http://poleiro.info/posts/2013-04-03-parse-errors-as-type-errors.html.

This is not as convenient to use as Coq's notations, since the term
that is produced in the end involves an explicit call to the parser.
Still, it might come in handy in some cases.

2014-10-11 19:47 GMT-04:00 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.



-- 
Arthur Azevedo de Amorim