export and namespaces

Stream: general

[Eric Wieser]

I'm seeing some odd behavior with the export command when used inside a namespace; it seems to allow things to be put in a namespace that can then only be retrieved with open, and not via dot notation:

def foo.bar : ℕ := 3

namespace nat
  export foo (bar)
end nat

#check (3 : ℕ).bar -- fail [ :( ]
#check nat.bar  --fail [ :( ]
#check bar -- fail [ expected ]

open nat

#check (3 : ℕ).bar -- fail [ expected, given the above ]
#check nat.bar -- fail [ expected, given the above ]
#check bar -- ok [ what? ]

Is this deliberate?