Stream: Coq users

Topic: Rejecting alphanumeric notations + identifier without a s...


view this post on Zulip 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 ']'").

view this post on Zulip Paolo Giarrusso (Jul 05 2022 at 18:14):

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 *)

view this post on Zulip Paolo Giarrusso (Jul 05 2022 at 18:15):

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.

view this post on Zulip Paolo Giarrusso (Jul 05 2022 at 20:26):

Posted on https://github.com/coq/coq/issues/4712#issuecomment-1175466710 which seems most related.

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Jul 05 2022 at 20:37):

Fair enough, fixed here and on github.


Last updated: Jun 14 2024 at 18:01 UTC