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.
Posted on https://github.com/coq/coq/issues/4712#issuecomment-1175466710 which seems most related.
the Definition A should be before the Fail otherwise it doesn't test quite the right thing
Fair enough, fixed here and on github.
Last updated: Sep 28 2023 at 10:01 UTC