Janno (Mar 30 2022 at 08:28): Janno (Mar 30 2022 at 08:28):Is it expected that notations using custom entries conflict with constr parsing?
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.
Guillaume Melquiond (Mar 30 2022 at 08:45):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?
Janno (Mar 30 2022 at 08:50):I think this solves my problem. Thank you very much!
Guillaume Melquiond (Mar 30 2022 at 09:01):Janno said:
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.
Paolo Giarrusso (Mar 30 2022 at 09:03):@Janno how does this solve the problem? IIUC, everything within quotes is a keyword?
Janno (Mar 30 2022 at 09:04):No, it seems only the first item in quotes needs to become a keyword. The suggestion does not make this a keyword.
Paolo Giarrusso (Mar 30 2022 at 09:06):O_O. Is this documented anywhere?
Michael Soegtrop (Mar 30 2022 at 09:09):Out of curiosity: do the quotes around the [ make a difference?
Janno (Mar 30 2022 at 09:10):I don't think it makes a difference
Paolo Giarrusso (Mar 30 2022 at 09:11):https://coq.inria.fr/refman/user-extensions/syntax-extensions.html#basic-notations would also suggest "no difference", but it doesn't mention keywords...
Paolo Giarrusso (Mar 30 2022 at 09:11):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.
Ali Caglayan (Mar 30 2022 at 13:02):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