feat: look if names are internal details

leanprover · Oct 16, 2024 · d36b7fd · d36b7fd
1 parent ccb4e97
commit d36b7fd
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/DocGen4/Process/DocInfo.lean b/DocGen4/Process/DocInfo.lean
@@ -124,6 +124,7 @@ def isBlackListed (declName : Name) : MetaM Bool := do
     pure (declName.isInternal)
     <||> (pure <| isAuxRecursor env declName)
     <||> (pure <| isNoConfusion env declName)
+    <||> (pure <| declName.isInternalDetail)
     <||> isRec declName
     <||> isMatcher declName
   -- TODO: Evaluate whether filtering out declarations without range is sensible