The Coq mailing list

[Daniel de Rauglaudre <daniel.de_rauglaudre AT inria.fr>]

Hi all,

I am a volunteer to implement it, if nobody minds. I started looking
at it.

On Fri, Feb 19, 2016 at 04:52:44PM -0500, 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

-- 
Daniel de Rauglaudre
http://pauillac.inria.fr/~ddr/