Patterns for auto generated declarations

Stream: lean4

[Henrik Böving]

While doing some experimentation for doc-gen4 i noticed that if you list the names of all the axioms and functions that are in e.g. the current mathlib4 quite a lot (I didnt check if it might even be the majority) of them seem to be autogenerated (at least from the way their name looks) and thus not exactly interesting to doc-gen4.

Now I'm guessing I could start digging through the compiler to find all spots that auto generate some names and write a function that is able to detect these auto generated declarations but I figured someone here will probably already know how auto generated names look (hopefully)?

[Siddhartha Gadgil]

Here is an extract from the lean4 source which I used to avoid auto-generated names by lean (which may be the same things that you want to avoid).

private def isBlackListed (declName : Name) : MetaM Bool := do
  let env ← getEnv
  (declName.isInternal && !isPrivateName declName)
  <||> isAuxRecursor env declName
  <||> isNoConfusion env declName
  <||> isRec declName
  <||> completionBlackListExt.isTagged env declName
  <||> isMatcher declName

[Henrik Böving]

Thanks! I'll add that to my code and see whether stuff starts disappearing.