The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

Thanks, Robbert.  Unfortunately, I guess this means "not without a 
plugin".  Instead, I'll just define hopefully enough numbers via 
Notations...

-- Jonathan


On 02/19/2016 04:59 PM, Robbert Krebbers wrote:
> Hi Jonathan,
>
> The parsers for numerals are implemented in OCaml. See for example 
> plugins/syntax/nat_syntax.ml in the Coq source tree.
>
> Best,
>
> Robbert
>
> On 02/19/2016 10:52 PM, Jonathan Leivent wrote:
> > Is there a way in Coq to overload the natural number notations? There
> > seems to be, because 42 in Z_scope is a Z, and 42 in bigZ_scope is a
> > BigZ.t_.  However, in neither case is the Notation "42" itself defined.
> > At least in the case of bigZ_scope, the only notations defined are "0",
> > "1" and "2" (in Numbers/Integer/BigZ/BigZ.v) - and those are Local.  So,
> > what magic makes it work for all other natural number notations as
> > well?  And can it be used for user-defined types?
> >
> > -- Jonathan