isBlackListed

Mathlib.Lean.Expr.Basic

URI: https://scilib.ai/kg/mathlib#Lean.Name.isBlackListed

Lean4

def isBlackListed {m} [Monad m] [MonadEnv m] (declName : Name) : m Bool :=
  (do
      if declName == ``sorryAx then
        return true
      if declName matches .str _ "inj" then
        return true
      if declName matches .str _ "noConfusionType" then
        return true
      let env ← getEnv
      pure <| declName.isInternalDetail || isAuxRecursor env declName || isNoConfusion env declName) <||>
    isRec declName <||> isMatcher declName

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

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

Разделы

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

Аффилиация

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