Should duplicated class projections be private?

Stream: mathlib4

[Jovan Gerbscheid]

Yaël Dillies said:

Jovan Gerbscheid said:

Should we use export LinearOrder (le_total min_def max_def) instead of having two identical lemmas in the root and LinearOrder namespaces? The duplication is a bit annoying for tagging.

It's useful to not use export because then the lemmas show up under the expected name in the docs (hopefully doc-gen can be fixed to avoid needing this hack)

Now that we have the module system, should we make LinearOrder.le_total, LinearOrder.min_def and LinearOrder.max_def private/not exported? I think this pattern of having a class projection duplicated in the main namespace is reasonably common in mathlib, and it would be nice to hide it from anyone importing this.

[Jovan Gerbscheid]

I tried it out, but it seems that if I mark a class projection as private, then the .mk class constructor is also marked private, which we obviously don't want.

Would it be a reasonable feature to allow marking structure projections as private, without marking the constructor as private?