imports and namespaces

Stream: lean4

[Paige Thomas]

Is there a way to reference a definition or theorem by the path from the root of the project to the file that it is in?

[Patrick Massot]

No, those are separate hierarchies. You could probably meta-program something, but this is really not how Lean is meant to be used. This is probably an #xy problem and we will probably be able to give a more helpful answer if you provide more context.

[Paige Thomas]

I think Lean wants me to have a single file that imports all of the other files in the project? This seems to require that I make sure there are no duplicate theorem and definition names in the project, but I'm not sure how to achieve that without making long names like substitution_theorem_sub_pred_all_rec_opt, so that I don't have two occurrences of substitution_theorem in the project.

[Patrick Massot]

You can use namespaces for that.

[Paige Thomas]

where one substitution_theorem is in one file, and another is in another file.

[Paige Thomas]

When I use namespaces, and make the file that imports all of the other files, I seem to still get clashes.

[Paige Thomas]

as an aside, what is the file that imports all of the other files used for?

[Paige Thomas]

Well, this is embarrassing. I can't seem to reproduce it.

[Paige Thomas]

Sorry.