blacklistInsertion

Mathlib.Lean.Meta.RefinedDiscrTree.Initialize

URI: https://scilib.ai/kg/mathlib#Lean.Meta.RefinedDiscrTree.blacklistInsertion

Lean4

/-- Return true if `declName` is automatically generated,
or otherwise unsuitable as a lemma suggestion. -/
def blacklistInsertion (env : Environment) (declName : Name) : Bool :=
  declName.isInternalDetail || declName.isMetaprogramming || !allowCompletion env declName ||
        Linter.isDeprecated env declName ||
      declName == ``sorryAx ||
    (declName matches .str _ "inj" | .str _ "injEq" | .str _ "sizeOf_spec")

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru