Opening namespace causes ambiguity

Stream: new members

[Mark Fischer]

So, in one file I've created a namespace to define functions without clashing with std names. Is there some way to open a namespace without those name clashes immediately coming back? I'd like to avoid prefixing everything I've defined within a namespace all the time.

[Mark Fischer]

What I'm getting right now:

ambiguous, possible interpretations
  _root_.or_assoc [...]
  MyLogic.or_assoc [...]

[Patrick Massot]

I'm not sure what you are asking for. Maybe you want open foo (bar) which makes bar accessible instead of foo.bar but nothing else from the foo namespace. Or open foo hiding bar which does the opposite.

namespace foo

def bar : Nat := 0

def baz : Nat := 1

end foo

section
open foo (bar)

#check bar -- works
#check baz -- fails
end

section
open foo hiding bar

#check bar -- fails
#check baz -- works
end

[Ruben Van de Velde]

I think the goal is to hide the root versions in favor of the MyLogic ones, which I'm not sure is possible

[Mark Fischer]

I'd like to be able to write:

open MyLogic
#check or_assoc

but right now that's ambiguous. Yes, @Ruben Van de Velde has it right.

[Mark Fischer]

So I've just noticed that the following seems to work:

namespace MyLogic
#check or_assoc