Théo Winterhalter (Jan 06 2021 at 09:37): Théo Winterhalter (Jan 06 2021 at 09:37):I have a problem with notations with the following example:
Notation " 'foo' " := 0 (at level 2).
Definition foo := 1.
The definition simply doesn't parse because foo has now a special role in the grammar. Is there a way around it?
Théo Winterhalter (Jan 06 2021 at 11:26):I don't expect to solve this problem for notations in general, but at least for custom entries. But even adding foo as a symbol for custom entries will yield the same problem.
Enrico Tassi (Jan 06 2021 at 11:27):foo is now a keyword
Enrico Tassi (Jan 06 2021 at 11:28):So it can't be an IDENT
Théo Winterhalter (Jan 06 2021 at 11:30):Yes, I understand the problem. Maybe I should explain what I want to do. I want to use custom entries to represent programs, and there I would like to use bool to represent the deeply embedded boolean type, but if I do it, then bool cannot be an indent.
Enrico Tassi (Jan 06 2021 at 11:30):The lexer is only one for all syntactic categories, so it does not matter where you add your notation
Théo Winterhalter (Jan 06 2021 at 11:30):I guess it's because of the lexer.
Enrico Tassi (Jan 06 2021 at 11:31):The usual workaround is to use "'bool" or "`bool" instead of "bool"
Théo Winterhalter (Jan 06 2021 at 11:31):I see. Thanks.
Enrico Tassi (Jan 06 2021 at 11:31):IIRC abbreviations, like Notation foo := 0 cannot be in a scope (but I may be wrong)
Enrico Tassi (Jan 06 2021 at 11:32):These don't add keywrods
Théo Winterhalter (Jan 06 2021 at 11:33):Yeah it doesn't seem to like the (in custom entries foo).
Guillaume Melquiond (Jan 06 2021 at 12:20):That said, I don't see any good reason for abbreviations to not be in scope. So, perhaps this limitation could be lifted.
Enrico Tassi (Jan 06 2021 at 14:15):There could even be a PR doing that, CC @Hugo Herbelin
Matthieu Sozeau (Jan 06 2021 at 16:00):Guillaume Melquiond said:
That said, I don't see any good reason for abbreviations to not be in scope. So, perhaps this limitation could be lifted.
I would like that too
Hugo Herbelin (Jan 06 2021 at 16:05):Enrico Tassi said:
There could even be a PR doing that, CC Hugo Herbelin
There are a couple of pending PRs on notations but not about abbreviations in scopes. That's probably feasible without too much trouble.
The issue with keywords having a side effect much beyond the area in which they are supposed to have a role, is otherwise a serious issue too. Probably solvable by merging lexing and parsing, as was discussed somewhere on Zulip.
Last updated: Apr 19 2024 at 19:02 UTC