sections vs namespaces

Stream: new members

[Arthur Paulino]

What's the difference between sections and namespaces?

[Kyle Miller]

Roughly, every namespace is a section that also puts the enclosed definitions and theorems into that namespace. For example, if f is defined within namespace foo, outside the namespace you refer to it as foo.f. You can also "open" namespaces to include everything defined in them. If you open foo, then you can refer to either foo.f or f.

https://leanprover.github.io/reference/other_commands.html#sections (and the next section)

[Kyle Miller]

(Lean has both a module system and a namespace system, and they're orthogonal concepts. Each module (a file) can import other modules and also define things in any number of namespaces. Contrast this with Java, which has a package system that merges the concepts of modules and namespaces. Python also merges these.)

[Arthur Paulino]

Thanks!