Go to definition for namespace names

Stream: lean4

[Julian Berman]

Consider a file containing:

-- uncomment me to instead jump to Lean/Elab/BuiltinCommand.lean
-- import Lean

#check Nat

namespace Nat
end Nat

and place your cursor on Nat on the namespace line and try jumping to definition. With no imports, this jumps nowhere. With the Lean import it jumps to Lean/Elab/BuiltinCommand.lean. I think in both cases I'd expect this to jump to the definition of Nat. Is this behavior known, desirable, best-possible-at-the-minute etc. and/or would an issue proposing to change it be welcome?

[Damiano Testa]

I would like it if it jumped to the definition of Nat, but I would honestly not expect it to!

[Kim Morrison]

Please open an issue! Both of the current outcomes are bad, and should be readily fixable.

[Julian Berman]

lean4#5298