Inaccessible usernames for local decls

Stream: lean4

[Thomas Murrills]

I'm wondering what exactly causes a local decl's username to be inaccessible by user syntax (i.e. through ident). LocalContext.inaccessibleFVars takes the stance that an fvar is inaccessible if it has macro scopes or is shadowed, but isInaccessibleUsername only checks if it has "✝" or "_inaccessible" in its outermost string part.

.anonymous (and .anonymous with numbers) seems to be inaccessible in practice, but is not considered inaccessible by either of these, and looks distinctively odd in the infoview, so perhaps the hope is that it never appears as a local decl username in the first place.

As far as I can tell, names ending in .numbers are also inaccessible via user syntax, but aren't treated that way by either of these functions or in the infoview. (Is there a roundabout way to access them within ident somehow?)

There might also be a line between "accessible" and "guillemet-accessible".

My motivation here is basically just "know which fvars could conceivably be accessed by user syntax". :)