Is there a way to import only one item from a module

Stream: general

[Ben]

I want to use a single function from a module. I don't want the other items to "pollute" the current file system namespace. Is there an import ... only [x] feature?

[Asei Inoue]

why don’t use private modifier?

[Jireh Loreaux]

If I understand correctly, this is on Sebastian Ullrich's roadmap for this year.

[Jz Pan]

Asei Inoue said:

why don’t use private modifier?

But there is from MODULE import FUNC1, FUNC2 in Python...

[Michael Rothgang]

There is open Foo (bar) - which brings only the item Foo.bar into scope. (to clarify: this is in Lean)

[Ruben Van de Velde]

But this is not python