Syntax declaration causes parsing error

Stream: lean4

[Yicheng Qian]

How can we define a custom syntax containing an identifier prefix while not causing parsing problems? For example, if I define

syntax foo := "foo"
syntax (name := bar) "bar" foo : tactic

then

#check (fun (foo : Nat) => foo)

produces error "expected ')' or term". Is there any way to fix this?

[Mario Carneiro]

does using &"foo" work?

[Yicheng Qian]

Oh it works!

[Mario Carneiro]

it should work in this case, but I don't know whether the real example is more complex

[Yicheng Qian]

What does & stand for?

[Mario Carneiro]

nonReservedToken instead of token

[Yicheng Qian]

Ok, it also works in the real example.

[Mario Carneiro]

the limitation of nonReservedToken is that it will not be differentiated from an ident in the same position

[Yicheng Qian]

Ok, I see. If a token is reserved then it cannot be ident, but if it's not reserved, then the corresponding string can represent either the token or an ident.