Leading parser

Stream: new members

[yichi zhou]

I'm trying to understand the parser of Lean 4. It seems there is a special parser named leading_parser. However, I'm not able to find the definition of leading_parser by neither GotoDefinition in vscode or searching in the lean 4 repo, as well as search in this forum.

Could anyone give me some references about it ?

[Kyle Miller]

leading_parser is a macro (more precisely, an elaborator) that wraps the parser in docs#Lean.Parser.leadingNode using the current declaration name as the syntax kind. It also sets up antiquotation handling in syntax quotations for this syntax kind.

docs#Lean.Elab.Term.elabLeadingParserMacro is the elaborator definition. The main work occurs in the function that's right before it.

[Kyle Miller]

By the way, leading_parser is meant to be used internally, from before the syntax command was available.