Defining non-reserved syntax

Stream: lean4

[Andrés Goens]

I'm trying to define custom syntax but don't want the keyword to be parsed somewhere else. Lean seems to have a parser for that, Parser.nonReservedSymbol, but it doesn't seem to work if I declare it with the syntax syntax:

declare_syntax_cat foo

def keywordParser := Parser.nonReservedSymbol "keyword"
syntax keywordParser : foo
syntax "[foo|" foo "]" : term

#check [foo| keyword] -- error: expected foo

I've seen the uses in Lean itself use some @[builtinAttrParser] annotations and leading_parser, but adding does doesn't seem to help (and I have no idea what they mean). Can someone tell me what I'm doing wrong? Thanks!

[Jannis Limperg]

This is the magical (behavior := both):

declare_syntax_cat foo (behavior := both)

syntax &"keyword" : foo
syntax "[foo|" foo "]" : term

#check [foo| keyword]

This option makes the syntax category parse leading identifiers as non-reserved symbols (and also as identifiers, if no non-reserved symbol matches). Imo this should be the default.

Also, note the &"bla" notation, which is a nicer way to write Parser.nonReservedSymbol "bla". In general, syntax is one area where I wouldn't look too much at the Lean 4 codebase itself. It largely uses low-level APIs instead of the nice syntax declarations, quotations and such. Look at mathlib4 code instead.