namespace mirroring folder structure

Stream: lean4

[Paige Thomas]

Is there a shortcut to declare a namespace that mirrors the folders that a file is contained in? For instance, if we have path/to/Blah.lean to declare a namepace in Blah.lean of path.to.

[Kyle Miller]

No, this doesn't exist -- modules and namespaces are meant to be orthogonal organizational concepts. It's possible to implement such a namespace command as a user though.

[Paige Thomas]

I think I am supposed to have a single file at the top of the repo that imports all of the other files, but I have duplicated names of things across those files. Is the best approach to put them in different namespaces?

[Kyle Miller]

Yeah, you should avoid re-using names. You can use namespaces or make auxiliary things private.

[Paige Thomas]

Ok. Thank you.

[Kyle Miller]

Here's such a command by the way:

macro "module_namespace" : command => do
  let mod ← Lean.getMainModule
  `(command| namespace $(Lean.mkIdent mod))

It only works if you're at the top level of the file, otherwise it will malfunction and enter some namespace based on the module name inside whatever you're namespace you're currently in.

[Paige Thomas]

Thank you!