Syntax atoms beginning with a single quote

Stream: lean4

[František Silváši]

Is there any way to make: notation "\'" x => x work? i.e. use ' as the very first character of an atom; or do we always hit the codepath via Lean.Elab.Syntax.isValidAtom which explicitly prohibits this.

[Jakob von Raumer]

Did you get any reply? In my case I don't even need the result to be atomic. Trying to parse single ' like this, but Lean still seems to want to parse a character literal:

def singleSingleQuote : Parser := rawCh '\'' (trailingWs := false)

@[combinator_formatter singleSingleQuote]
def singleSingleQuote.formatter := PrettyPrinter.Formatter.visitAtom Name.anonymous

@[combinator_parenthesizer singleSingleQuote]
def singleSingleQuote.parenthesizer := PrettyPrinter.Parenthesizer.visitToken

syntax singleSingleQuote noWs ident : kid

syntax "`[kid|" kid "]" : term

#eval `[kid|'foo]

[François G. Dorais]

I think this needs an RFC to Lean core.

[Jakob von Raumer]

cc @Sebastian Ullrich

[Sebastian Ullrich]

Do you need it at the beginning of a syntax category? The above category only has one production so it's not really necessary in that specific example

[Jakob von Raumer]

Ah, I guess I can avoid that

[Jakob von Raumer]

Works! Why does that make a difference?

[Sebastian Ullrich]

The production of the syntax category is chosen via parseToken. So it might also work if Parser.info is set up correctly for your custom parser.

[Jakob von Raumer]

Jakob von Raumer said:

Ah, I guess I can avoid that

Can avoid that in that syntax category, but to not have it at the start of any syntax category upwards from it is close to impossible. Will look at the Parser.info

[Sebastian Ullrich]

Not sure I understand that, if it's not at the beginning of the immediately surrounding category, how can it be at the beginning further up the stack?

[Jakob von Raumer]

Eh, my "solution" was to turn the category that's called kid in the example above into a straight ParserDescr instead of a syntax category, but that just shifts the problem.

[Jakob von Raumer]

The production of the syntax category is chosen via parseToken.

Did you really mean parseToken? I can only find tat in the formatter :thinking: