RFC: private/public/protected in local where/let rec

[nomeata]

Proposal

While local let declarations are properly private, local where and let rec declarations float to top-level definitions (namespaced within the enclosing definiton’s name).

To downstream tooling (doc generation, linters), these look like normal public definitions, e.g show up in the module API description. I find this surprising, and would assume them to be an implementation detail of the enclosing function, and not or only hard to get your hands on from the outside.

One possible fix is to treat them always like private definitions (as experimented with in #2717). But there seem to be use case where you do want outside access to local definitions (otherwise why would docstrings be supported, and presumably in proofs it might be useful).

A more refined fix is to allow the visibility modifiers public, private and protected to be used in where and let rec, giving the developer control over whether these definitions should or should not be externally visible. Possibly with private being the default.

Another direction would be to simply somehow mark these definitions as “lifted from local definitions”, and let the tooling decide what to with it (e.g. the docstring linter could not complain about them; the API documentation could omit them unless there is a docstring).

Community Feedback

Previously briefly discussed on Zulip.

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

[kmill]

It would be good to compare this to some other solutions, for example Lean could provide an attribute it applies to auxiliary definitions, and downstream tools could take this into account. Or, Lean could annotate the names in such a way that downstream tools can see these are auxiliary (like perhaps prepending with an underscore, which is a pre-existing way to make it be an "internal" name).

Regarding visibility modifiers, one of the rules of thumb in mathlib is that you never want any definitions to be private, since there's a good chance you'll want to prove something about the definition eventually. Definitions made with let are not "private" per se, since their entire definition is embedded in the host definition inside the let expression. Definitions made with let rec are hoisted to being top-level definitions so that they can be compiled with the equation compiler. There's also the question of what Lean is supposed to do if you have a private definition with a public definition in a where clause.

There are other bits of syntax that generate auxiliary top-level definitions as well, for example match expressions. Downstream tools use heuristics to decide whether a top-level definition is auxiliary. For example, Name.isInternal and Docgen's isBlacklisted.

[nomeata]

That makes sense, so a should-appear-in-documentation vs. should-not-appear-in-documentation marker, orthogonal to the existing visibility flags, could be useful? Especially if let rec definitions have the should-not-appear-in-documentation attribute by default, but allow it to be changed back explicitly. If we want different defaults for normal vs. lifted definitions, this needs to be an attribute known to Core, right?