Namespace best practice

Stream: general

[Martin Dvořák]

Do you create a global namespace for your entire project?
I'm creating a reüsable Lean 3 library.
I don't have any custom namespaces inside it.

[Mario Carneiro]

It is entirely up to you. If the names you want to use could reasonably be taken by something else then they should be namespaced, and namespacing the whole project is an easy way to avoid conflicts. Just consider how the user will use your library and what they would prefer