@Kha The default value (false) for `pp.inaccessibleNames == false` help when
visualizing error messages (see test
`hidingInaccessibleNames.lean`). We added this feature after to hide
intermediate variables created by `match_syntax`.
However, this default value confused me in tactic mode. For example,
it will hide a hypotheses `x : Fin 0` if nobody depends on it, but as
a user we want to know we have it since we can close the goal using
it. Thus, I added `withPPInaccessibleNames act`, it executes `act`
using `pp.inaccessibleNames true` if the user did not explicitly set
it. I use this combinator at `FileWorker` and when producing the
`unsolved goals` error message. In all other scenarios, I believe
hiding these inaccessible variables is a good thing.
880f1372bd