Zulip Chat Archive

Stream: general

Topic: export and namespaces


view this post on Zulip Eric Wieser (Mar 30 2021 at 10:45):

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?


Last updated: May 11 2021 at 13:22 UTC