Is it expected that notations using custom entries conflict with
Declare Custom Entry e. Notation "'[this' := x ]" := (x = x) (in custom e, x constr). From Coq Require Import List. Import List.ListNotations. Succeed Check fun that : nat => [that] : list nat. Fail Check fun this : nat => [this] : list nat.
(Note that the notation is entirely unused in the example and its body doesn't matter.)
I was under the impression that custom entries lived in different parsing tables. I already know the notion of a keyword is shared but I didn't know that even non-keywords can cause conflicts.
But that is not a non-keyword. You are actually defining a new keyword. Did you perhaps mean the following?
Notation "'[' 'this' := x ]" := (x = x) (in custom e, x constr).
Oh! Interesting! I guess I was going by the absence of a warning about defining a new keyword. Maybe these only show up for keywords that could also be regular names?
I think this solves my problem. Thank you very much!
Maybe these only show up for keywords that could also be regular names?
Yes, identifiers and numbers. That said, it has been a long time since I last saw this warning. I wonder if it has not been inadvertently removed.
@Janno how does this solve the problem? IIUC, everything within quotes is a keyword?
No, it seems only the first item in quotes needs to become a keyword. The suggestion does not make
this a keyword.
O_O. Is this documented anywhere?
Out of curiosity: do the quotes around the
[ make a difference?
I don't think it makes a difference
https://coq.inria.fr/refman/user-extensions/syntax-extensions.html#basic-notations would also suggest "no difference", but it doesn't mention keywords...
The notation consists of tokens separated by spaces. Tokens which are identifiers (such as A, x0', etc.) are the parameters of the notation. Each of them must occur at least once in the abbreviated term. The other elements of the string (such as /\) are the symbols.
Identifiers enclosed in single quotes are treated as symbols and thus lose their role of parameters.
When notations are being searched there is a process that unqoutes a notation string, and replaces free(?) terms with underscores. So
'this' x would get processed to
this _ and that is how the notation is looked up in a table. Of course not every method processing notations does the same things, so take this explanation with a pinch of salt. I only found out about this when working on implementing the
Print Notation command.
Last updated: Sep 26 2023 at 12:02 UTC