namespace Foo

def Bar.bar : Nat := 1

export Bar (bar)

def boo := 2

end Foo

namespace Baz

#check Foo.bar

open Foo in
#check bar

section Ex1
open Foo (bar)
#check bar
#check boo -- should fail
end Ex1

section Ex2
open Foo hiding bar
#check bar -- should fail
#check boo
end Ex2

section Ex2
open Foo renaming bar → bah
#check bah
end Ex2

export Foo (bar)
export Foo.Bar (bar)
#check bar

end Baz