Stream: Coq users

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


view this post on Zulip 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?

view this post on Zulip Guillaume Melquiond (Jun 25 2021 at 13:43):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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: Jan 29 2023 at 01:02 UTC