Exclude private as implementation detail

Stream: metaprogramming / tactics

[Daniel Weber]

I'm processing names, and I'm using docs#Lean.Name.isBlackListed to check if they are implementation detail and should be skipped over. However, this also skips over user-defined private constants, and I do want to keep those. How can I do that?

[Daniel Weber]

I can try to apply docs#Lean.privateToUserName? before, but then it doesn't filter enough, and keeps, for instance, _private.Init.Data.List.BasicAux.0.List.get.match_1.splitter