Stream: Coq users

Topic: Bad interaction with notation and names


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

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

view this post on Zulip Enrico Tassi (Jan 06 2021 at 11:27):

foo is now a keyword

view this post on Zulip Enrico Tassi (Jan 06 2021 at 11:28):

So it can't be an IDENT

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

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

view this post on Zulip Théo Winterhalter (Jan 06 2021 at 11:30):

I guess it's because of the lexer.

view this post on Zulip Enrico Tassi (Jan 06 2021 at 11:31):

The usual workaround is to use "'bool" or "`bool" instead of "bool"

view this post on Zulip Théo Winterhalter (Jan 06 2021 at 11:31):

I see. Thanks.

view this post on Zulip Enrico Tassi (Jan 06 2021 at 11:31):

IIRC abbreviations, like Notation foo := 0 cannot be in a scope (but I may be wrong)

view this post on Zulip Enrico Tassi (Jan 06 2021 at 11:32):

These don't add keywrods

view this post on Zulip Théo Winterhalter (Jan 06 2021 at 11:33):

Yeah it doesn't seem to like the (in custom entries foo).

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

view this post on Zulip Enrico Tassi (Jan 06 2021 at 14:15):

There could even be a PR doing that, CC @Hugo Herbelin

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

view this post on Zulip 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: Feb 08 2023 at 22:03 UTC