private access

Stream: lean4

[Joseph O]

If I mark a function private, can it only be accessed within that namespace or section and nowhere else, or is it not that strict?

[Simon Hudon]

Those declarations are still in the environment after the namespace is closed but its name is mangled. If you defined it as Namespace.foo and defined it in dir/file.lean, it will be in your environment as dir.file.0.Namespace.foo (or with another number if there are multiple private definitions with the same name in the same file).

[Gabriel Ebner]

If you're using mathlib4, you can also do open my.private.defn from Module.Where.Its.Defined.In to comfortably access private definitions from other modules.