Unexpected difference between charLit and strLit parsers

Stream: lean4

[François G. Dorais]

Consider this mwe:

open Lean Parser

macro "strTest" s:strLit : term => if s.getString = "T" then `(true) else `(false)

macro "testChar" c:charLit : term => if c.getChar = 'T' then `(true) else `(false)

The first works because the strLit parser returns TSyntax `str but the charLit parser returns TSyntax `Lean.Parser.charLit instead of TSyntax `char.

Is there a reason for this difference?

[Kyle Miller]

It looks like strLit is special cased in docs#Lean.Elab.Command.expandMacroArg.mkAntiquotNode and charLit isn't

[François G. Dorais]

Thanks! I was having a really had a hard time figuring out where that was from!

I'm not sure that's a bug but I'll submit a report anyway...