Recently I ran into this isssue:
But it begs the question, is it good design to have modules with keyword names? I believe that
Should be accepted but gives:
Syntax error: [export_token] expected after 'Module' (in [gallina_ext]).
Are there any technical reasons for not doing so?
That would be way too confusing, since
Module Type already denotes a functor definition.
The thing is we can already create
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.
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
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