Get full name of declaration

Stream: lean4

[Tomas Skrivan]

How do I get the full name of a declaration in macro/elaborator?

import Lean
open Lean Parser

namespace Foo
  def foo := 1
end Foo
open Foo

elab "#print_full_name" n:ident : command => do
  IO.println s!"short name: {n}"
  IO.println s!"full name: {n}" -- how do I get `Foo.foo ?

#print_full_name foo

I want the above to output

short name: foo
full name: Foo.foo

[Damiano Testa]

If there is only one possiblity, this works:

elab "#print_full_name" d:declId : command => do
  let nd ← Lean.resolveGlobalConstNoOverload d.raw[0]
  IO.println nd

#print_full_name foo

[Damiano Testa]

Otherwise, removing the NoOverload will give you a list of possibilities.

[Tomas Skrivan]

Thanks, that is exactly the function I was looking for!

[Kyle Miller]

Why a declId @Damiano Testa ? That includes universe information, which you're dropping. You can do this too:

elab "#print_full_name" d:ident : command => do
  let nd ← Lean.resolveGlobalConstNoOverload d
  IO.println nd

[Tomas Skrivan]

Because I had declId in my original question

[Tomas Skrivan]

But then realised that it should be just ident and simplified the mwe