nonReservedSymbol syntax

Stream: lean4

[Kenny Lau]

Is there a syntax for nonReservedSymbol?

open Lean

#check `(ident|X)

syntax foo := "X"
syntax "#asdf " foo : command

#check `(ident|X)

Basically I want to be able to still use X as an identifier after declaring it as part of the foo syntax

[Damiano Testa]

Is adding a & before the symbol what you are looking for?

[Kenny Lau]

aha!

[Kenny Lau]

@Damiano Testa do you know where this is documented?

[Damiano Testa]

I'm not sure and I'm not at a computer. Does hovering say something?

[Kenny Lau]

no it just links me back to nonReservedSymbol

[Kyle Miller]

It's mentioned here at least: https://lean-lang.org/doc/reference/latest/Notations-and-Macros/Defining-New-Syntax/#Lean___Parser___Syntax___nonReserved (a brief description is in the paragraph right before the anchor target)