opening namespaces

Stream: mathlib4

[Johan Commelin]

MWE

def Nat.Foo : Type := Bool

def Nat.Bar : Type := Int

theorem Bar.lemma1 : True := trivial

theorem Nat.Bar.lemma2 : True := trivial

namespace Nat.Foo

open Bar

#check lemma1 -- unknown identifier 'lemma1'
#check lemma2 -- works

open _root_.Bar -- unknown namespace '_root_.Bar'

end Nat.Foo

[Johan Commelin]

This problem shows up in https://github.com/leanprover-community/mathlib4/pull/3833 where we want to open Primrec, but the effective result is open Nat.Primrec.

cc @Pol'tta / Miyahara Kō

[Johan Commelin]

Is this a known issue? Is there a workaround available?

[Reid Barton]

I think this behavior gets used a lot, e.g., open Lean Meta or whatever it is

[Johan Commelin]

I see. But is there a way top open non-nested namespaces that conflict namewise with nested ones?