feat: Use private names in where and local let

[nomeata]

(no need to look yet, running this to see what breaks)

Motivation:

Hide local definitions from generated documentation, and prevent docstring
linters from complaining about missing docstrings in where clauses.

[nomeata]

Some tests fail, for example ./tests/lean/run/inlineWithNestedRecIssue.lean:

import Lean

@[inline] private unsafe def mapMonoMImp [Monad m] (as : Array α) (f : α → m α) : m (Array α) :=
  go 0 as
where
  @[specialize] go (i : Nat) (as : Array α) : m (Array α) := do
    if h : i < as.size then
      let a := as[i]
      let b ← f a
      if ptrEq a b then
        go (i+1) as
      else
        go (i+1) (as.set ⟨i, h⟩ b)
    else
      return as

set_option trace.Compiler.result true
#eval Lean.Compiler.compile #[``mapMonoMImp, ``mapMonoMImp.go]

So there is a need to access the local definitions from the outside. And test ./tests/lean/docStr.lean also shows that by design local definitions are available from the outside…

So maybe another way must be found to let documentation and linters recognize local definitions (and, for example, hide them from the API unless they have a docstring).

Or maybe local definitoins should support private, public, protected qualifiers, maybe even defaulting to private.