Zulip Chat Archive

Stream: lean4

Topic: private access


Joseph O (Feb 23 2022 at 03:08):

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 (Feb 23 2022 at 03:18):

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 (Feb 23 2022 at 08:37):

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.


Last updated: Dec 20 2023 at 11:08 UTC