prettyprint command quotation

Stream: lean4

[James Gallicchio]

MWE

import Lean

open Lean Elab Command
#eval show CommandElabM Unit from do
  let syn : Term ← `( `(command| def hi := sorry ) )
  let fmt ← liftCoreM <| Lean.PrettyPrinter.formatCommand syn
  IO.println fmt

formatCommand throws an error (unknown constant '«|»') because of the use of (command|. The same snippet with a generic quotation ( works fine.

I don't know enough about quotations or prettyprinting to have a good sense of what is going wrong here :frowning:

for my particular use case I can work around this, but figured I'd flag it

[Kyle Miller]

It seems to be that the pretty printer has no support for "dynamic quotations", which are ones that need to resolve the name before the |.

If you remove command|, then you can use a feature where `(...) falls back to trying to parse it as a command, and then it appears to work.