namespace shenanigans

Stream: lean4

[Kenny Lau]

axiom A.b : Nat

theorem A.h₁ : b = 0 := sorry -- correctly resolves to A.b

namespace E

theorem _root_.A.h₂ : b = 0 := sorry -- does not recognise b

end E

[Leni Aniva]

why should this resolve to b? To avoid surprises a definition should work the same way regardless of the name of the decl

[Kenny Lau]

for me it's the opposite, because when I write _root_.A i almost always mean "i actually wanted this to be under the namespace A but i was too lazy", so I would expect it to behave as if it was in the namespace A

[Kyle Miller]

issue lean4#9445 is possibly addressing this

[Kenny Lau]

Leni Aniva said:

why should this resolve to b? To avoid surprises a definition should work the same way regardless of the name of the decl

well this is false already, because in the above you can see how the name A.h₁ causes b to be resolved to A.b

[Niels Voss]

That's not my favorite design choice, but since it is already in Lean we should be consistent and adopt it for _root_ decls as well