pretty-printing Name

Stream: Is there code for X?

[Joachim Breitner]

What is the idiomatic way to say

logInfo m!"Something about {name}"

where name : Lean.Name when name refers to a global name, so that it becomes clickable in the info view?

[Kyle Miller]

Adapting some code for the #explode tactic, this seems to work:

open Lean Elab

def ppConst (n : Name) : MetaM MessageData :=
  try
    let n ← resolveGlobalConstNoOverloadCore n
    let e ← mkConstWithLevelParams n
    pure <| .ofPPFormat { pp := fun
      | some ctx => ctx.runMetaM <| withOptions (pp.tagAppFns.set · true) <|
          -- The pp.tagAppFns option causes the `delabConst` function to annotate
          -- the constant with terminfo, which is necessary for seeing the type on mouse hover.
          PrettyPrinter.ppExprWithInfos (delab := PrettyPrinter.Delaborator.delabConst) e
      | none     => return f!"{e}" }
  catch _ =>
    pure m!"{n}"

elab "test" : term => do
  logInfo m!"Something about {← ppConst `List.cons}"
  logInfo m!"Something about {← ppConst `List.cons'}"
  return mkSort .zero

#check test

[Joachim Breitner]

Thanks! That reminded me that there is a Lean.ppConst in std that I can use to write

 {ppConst (← mkConstWithFreshMVarLevels thm1)}

(which works fine, but is still a mouthful).

[Kyle Miller]

Oh, someone seems to have upstreamed that code I wrote for #explode to std :-)

[Kyle Miller]

By the way, use mkConstWithLevelParams instead, since that uses the level parameters from the declaration, rather than creating new metavariables. It looks nicer on hover, unless you do want to signify these are separate level parameters.

[Joachim Breitner]

It’s also shorter :-D