Using syntax with quotations

Stream: lean4

[Mario Carneiro]

For builtin notations defined with leading_parser like:

def fromTerm   := leading_parser " from " >> termParser

I find that I can write quotations targeting this syntax class using `(Parser.Term.fromTerm| from $stx), which is very convenient. But this does not seem to extend to definitions created with the more high level command syntax:

syntax binderIdent := ident <|> "_"

Here binderIdent itself has the type Lean.ParserDescr, unlike fromTerm which is a LeadingParser. As a result `(binderIdent| _) doesn't work. I'm also not sure if this command generates a parenthesizer / formatter; it is not in the obvious place if so.

[Mac]

Mario Carneiro said:

I'm also not sure if this command generates a parenthesizer / formatter; it is not in the obvious place if so.

It does. See here for how it generates a Parenthesizer and here for how it generates a Formatter.

[Mac]

Mario Carneiro said:

Here binderIdent itself has the type Lean.ParserDescr, unlike fromTerm which is a LeadingParser. As a result `(binderIdent| _) doesn't work.

I suspect this is merely an oversight. The problem is simply that evalParserConstUnsafe has no case for ParserDescr.

[Mac]

Though it is worth noting that adding such a case would require it needing to call something like compileParserDescr, which would likely require moving the definition of evalParserConstUnsafe (and, more importantly, parserOfStack) out of Lean.Parser.Basic so that it can import it.