Hey, I'm trying to add two notations:
Notation "E '[' e ']'" := (fill_hole E e) (at level 75).
Notation "e '[' y '/' x ']'" := (esubst x y e) (at level 80, y at level 10).
Unfortunately, they clash and I can't get them to work properly. Either I get "Unknown interpretation for
_ / _" for notations of the form "e[y/x]", or, if I wiggle the levels around, I get
'/' expected after [term level 10] for terms of the form "E[e]". I wonder what is necessary to make both coexist.
E differ in their types.
Thanks in advance!
Alright, I've managed to resolve this by virtue of more or less randomly changing levels and associativity.
Notation "E '[' e ']'" := (fill_hole E e) (at level 1, e at next level, no associativity). Notation "e '[' y '/' x ']'" := (esubst x y e) (at level 1, y at next level, left associativity).
...does the trick. :-)
FWIW that looks good but if you need it again: the rule is that priorities in the common prefix must be identical, and you probably want to spell them out to be sure.
This enables Coq to transform the grammar (by “left factoring”) to fit the limitations of the LL(1) parsing engine; the Coq manual does have a bit more info.
Thanks, Paolo. As Matthis did, I was also struggling to introduce new notations in Coq. I carefully read the reference manual, but I could not figure it out. Your comment is really helpful.
FWIW, the relevant section is https://coq.inria.fr/refman/user-extensions/syntax-extensions.html#simple-factorization-rules; improvements welcome.
Thank you for sharing the link. The reference manual (and maybe other experts) recommends
Print Grammar constr to see how the notations are defined, but I am not able to understand the output. To figure out the output, should I read https://camlp5.github.io/doc/htmlc/grammars.html ? (I think I need to study OCaml first.)
Yeah the Camlp5 manual is indeed helpful, especially for features like
OK. I'll try to read it. Thanks for your advice! :wink:
Last updated: Jan 28 2023 at 05:02 UTC