A command that prints the current namespace?

Stream: new members

[Eduardo Ochs]

Hi all,

how do I write a command that prints the current namespace? I guess that I would need elab, CoreM, logInfo, and getCurrNamespace, but I don't know how to put these pieces together...

Thanks in advance!

[Yaël Dillies]

Have you looked at how #where is implemented?

[Eduardo Ochs]

Is it from Lean itself or from mathlib? I don't have mathlib here now, and my usual ways of grepping the Lean sources don't show it...

[Yaël Dillies]

Hmm, don't actually know

[Damiano Testa]

I think that the namespace is stored in the Scope. You may be able to access it from CommandElabM.

[Damiano Testa]

Actually docs#Lean.Macro.getCurrNamespace may do just that for you.

[Eduardo Ochs]

Sorry for my newbieness, but how do I convert its output to a string? Try:

namespace Foo
#check Lean.Macro.getCurrNamespace
#print Lean.Macro.getCurrNamespace
#eval  Lean.Macro.getCurrNamespace
end Foo

The #eval fails...

[Damiano Testa]

Try something like #eval do logInfo (← Lean.Macro.getCurrNamespace) (untested).

[Damiano Testa]

import Lean

namespace Lean
run_cmd logInfo (← getCurrNamespace)

(tested!)

[Markus Schmaus]

Cool! To make this work in different namespaces as well, I just needed to use the Lean..

import Lean

namespace Foo
run_cmd Lean.logInfo (← Lean.getCurrNamespace)

[Kyle Miller]

If you add the open Lean command you don't need to add the Lean. prefix.