Stream: Coq users

Topic: Can/should modules be named as reserved words?

Ali Caglayan (Jun 25 2021 at 13:42):

Recently I ran into this isssue:
https://github.com/coq/coq/issues/14423
But it begs the question, is it good design to have modules with keyword names? I believe that

Module Type.

Should be accepted but gives:

Syntax error: [export_token] expected after 'Module' (in [gallina_ext]).

Are there any technical reasons for not doing so?

Guillaume Melquiond (Jun 25 2021 at 13:43):

That would be way too confusing, since Module Type already denotes a functor definition.

Ali Caglayan (Jun 25 2021 at 16:05):

The thing is we can already create Modules named Type just be calling the file that. But this is problematic since we cannot import it without giving the full logical name since coq doesn't accept Type as a module name.

Ali Caglayan (Jun 25 2021 at 16:05):

So it seems to me the correct behaviour should be to disallow files called Type or allow Type as a module name. The latter seems like the better option IMO

Stéphane Desarzens (Jun 25 2021 at 19:02):

There are other words with similar problems, but I don’t have an example ready. But they weren’t about modules, but about definitions...

Last updated: Oct 13 2024 at 01:02 UTC