Zulip Chat Archive
Stream: lean4
Topic: Inaccessible usernames for local decls
Thomas Murrills (Jun 28 2024 at 19:33):
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 .num
bers 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". :)
Last updated: May 02 2025 at 03:31 UTC