alias not respecting _root_

Stream: general

[Yaël Dillies]

Using _root_ when declaring an alias with alias doesn't actually put it in the root namespace, but appends a _root_ namespace:

namespace foo
def bar : true := trivial
alias bar ← _root_.baz
end foo

#check baz -- unknown identifier 'baz'
#check _root_.baz -- _root_.baz : true

[Kevin Buzzard]

Sounds like the perfect time for you to learn some C++ Yael!

[Eric Wieser]

Alias is written in Lean, isn't it?

[Anatole Dedecker]

That's because names declared by alias are always in the root namespace iirc

[Eric Wieser]

docs#tactic.alias.alias_cmd

[Yaël Dillies]

Aaah, okay. That makes sense

[Mario Carneiro]

when alias was written, it wasn't even possible for lean code to know what namespace you are in. It would be good if lean exposed its namespace name resolver to user code, but barring that it should be sufficient to work it out manually given the current namespace (which has a hook)