Check if a theorem is generated as a part of another one

Stream: metaprogramming / tactics

[Leni Aniva]

Is there a way to check if a theorem is generated as a part of another theorem?

e.g. _proof_123, match_1_1.

Using e.g. hasNum is not reliable.

[Yury G. Kudryashov]

There is docs#Batteries.Tactic.Lint.isAutoDecl

[Leni Aniva]

Yury G. Kudryashov said:

There is docs#Batteries.Tactic.Lint.isAutoDecl

This would detect private names as internal right? Name.isInternal uses the underscore prefix heuristic, which is true for private names. A user defined private name could be flagged as internal.