Names starting with `_`

Stream: lean4

[Jovan Gerbscheid]

The doc-string of Name.isInternal claims that

The frontend does not allow user declarations to start with `_` in any of its parts.
   We use name parts starting with `_` internally to create auxiliary names (e.g., `_private`).

However, if I type def _foo := 5, Lean doesn't complain. Should it?

As a result you can write names starting with _private., which Lean will think is a private name, even if it wasn't labelled with private.

[Jovan Gerbscheid]

The context here is that I want to write a theorem that is exported because it is needed by a tactic, but I don't want it to get a user facing name. One way to do this is to give it a name part that starts with _, similar to the typical ._simp_1 and .proof_1 lemmas.