namespace

Stream: new members

[Alex Zhang]

(deleted) (solved)

[Alex Zhang]

Is there a way to "protect" the identifier of the def from having the prefix name even though it is defined in the namespace block?

namespace name
def silly := 1
end name

#check name.silly
--#check silly

[Horatiu Cheval]

You can open the namespace so that you may refer to it without the prefix.

namespace name
def silly := 1
end name

open name
#check silly

[Horatiu Cheval]

Alternatively you can export it from the namespace so that it is available without also making all the identifiers in the namespace available.

namespace name
def silly := 1
end name

export name (silly)
#check silly

[Horatiu Cheval]

But with all this, the "true" full name of the identifier, as show by set_option pp.all true will still have the prefix, you just don't have to type it.

[Eric Wieser]

Are you looking for def _root_.silly := ...?

[Alex Zhang]

Eric Wieser said:

Are you looking for def _root_.silly := ...?

Exactly.