The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Is there a reason that files don't pack notations into scopes specific to the development, and then have one module which can be imported for notations which just opens the appropriate scopes and binds the appropriate scopes to the appropriate types?

-Jason

On Fri, May 17, 2013 at 11:46 AM, Pierre Boutillier <pierre.boutillier AT pps.univ-paris-diderot.fr> wrote:

Hi,
Le 17 mai 2013 à 17:15, CJ Bell <cbell AT CS.Princeton.EDU> a écrit :

>> Some people have started to pack their notations in submodules to that effect, but it doesn't work very well.
>
> Could you be more specific on this point? What problems would arise if
> the standard library adopted this approach?

I don't know what Arnaud has in mind and I do like this approach.
In fact, my point of view is a bit different, I think module shouldn't be "Import"ed. But you need to import notations in order to use them. That's why I've made a special module for things you want to import in Coq.Vectors.Vectors.

Anyway, I see an annoying point : Using notations in the module where you define stuff you make notations for asks for defining notations twice. As you can see, notations about vectors are defined twice. Once locally in order to be allowed to use [] and :: in VectorDef module but not disturb other modules and once in the correct module to make them publicly available.
>
>
> Thanks,
> -cj
All the best,
Pierre B.