Paolo Giarrusso (Jul 05 2022 at 18:08): Paolo Giarrusso (Jul 05 2022 at 18:08):It seems that after making \pre into a keyword (below), \preFoo (without a space) is parsed as \pre Foo instead of rejected as a syntax error. Can that be fixed, and should that happen in Coq or in my code?
Reserved Notation "'\pre' pre X"
(at level 10, pre at level 200, X at level 200, left associativity,
format "'[v' '[ ' '\pre' '/' pre ']' '//' X ']'").
Saddened by the discovery, I first balked at the idea of minimizing it — I didn't have the heart for it... But after a moment, I found back the courage and stared into the abyss:
Notation "'foobar'" := 1.
Definition a := foobar.
Definition A := 2.
Fail Definition b := foobarA. (* Good, as expected *)
Notation "'\foobar'" := (fun x => 1 + x).
Definition b := \foobarA. (* Nooo come on *)
it seems the lexer knows that at least pure alphabetic notations need be followed by some separators, like identifiers — but it doesn't know that expectatin for keywords that _end_ in alphabetic sequences.
Paolo Giarrusso (Jul 05 2022 at 20:26):Posted on https://github.com/coq/coq/issues/4712#issuecomment-1175466710 which seems most related.
Gaëtan Gilbert (Jul 05 2022 at 20:30):the Definition A should be before the Fail otherwise it doesn't test quite the right thing
Paolo Giarrusso (Jul 05 2022 at 20:37):Fair enough, fixed here and on github.
Last updated: Sep 28 2023 at 10:01 UTC