how to reserve syntax?

Stream: lean4

[Kenny Lau]

syntax small_spec := num
declare_syntax_cat step_group
syntax "small " small_spec : step_group
#check `(step_group|small 37)
def small : Nat := 37
#check small

I'm trying to define a custom syntax called "step_group", which for now contains things like small 37. The problem I'm facing is that after declaring it, somehow I can't use small anymore as an identifier even though the context has nothing to do with step_group; and if I make it non-reserved by putting &"small" in the syntax declaration, then suddenly it is not recognised as a correct syntax anymore.

[Aaron Liu]

Try declare_syntax_cat step_group (behavior := symbol) maybe?

[Aaron Liu]

I remember reading a docstring or something that was about how this works

[Aaron Liu]

ah yes docs#Lean.Parser.LeadingIdentBehavior docstring might have something to say

[Floris van Doorn]

Aaron Liu said:

Try declare_syntax_cat step_group (behavior := symbol) maybe?

Unfortunately nothing in that line has useful hover information, so it's not easy to jump to its definition. But the language reference does have a section discussing this as well:
https://lean-lang.org/doc/reference/latest/Notations-and-Macros/Defining-New-Syntax/?terms=declare_syntax_cat#syntax-categories

[Aaron Liu]

that's weird did they get rid of the hover information or was there none to begin with

[Floris van Doorn]

I expect it's a special syntax whose elaborator just doesn't put hover information over its syntax (probably because it was forgotten to add it).