isBlacklisted

Stream: mathlib4

[Joachim Breitner]

Should some of these be unified:

~/build/lean/mathlib4 $ git grep -10 def\ isBlackListed
Mathlib/Lean/Expr/Basic.lean-def isInternal' (declName : Name) : Bool :=
Mathlib/Lean/Expr/Basic.lean-  declName.isInternal ||
Mathlib/Lean/Expr/Basic.lean-  match declName with
Mathlib/Lean/Expr/Basic.lean-  | .str _ s => "match_".isPrefixOf s || "proof_".isPrefixOf s
Mathlib/Lean/Expr/Basic.lean-  | _        => true
Mathlib/Lean/Expr/Basic.lean-
Mathlib/Lean/Expr/Basic.lean-
Mathlib/Lean/Expr/Basic.lean-open Meta
Mathlib/Lean/Expr/Basic.lean-
Mathlib/Lean/Expr/Basic.lean--- from Lean.Server.Completion
Mathlib/Lean/Expr/Basic.lean:def isBlackListed (declName : Name) : MetaM Bool := do
Mathlib/Lean/Expr/Basic.lean-  if declName == ``sorryAx then return true
Mathlib/Lean/Expr/Basic.lean-  if declName matches .str _ "inj" then return true
Mathlib/Lean/Expr/Basic.lean-  if declName matches .str _ "noConfusionType" then return true
Mathlib/Lean/Expr/Basic.lean-  let env ← getEnv
Mathlib/Lean/Expr/Basic.lean-  pure $ declName.isInternal'
Mathlib/Lean/Expr/Basic.lean-   || isAuxRecursor env declName
Mathlib/Lean/Expr/Basic.lean-   || isNoConfusion env declName
Mathlib/Lean/Expr/Basic.lean-  <||> isRec declName <||> isMatcher declName
Mathlib/Lean/Expr/Basic.lean-
Mathlib/Lean/Expr/Basic.lean-end Name
--
Mathlib/Lean/Name.lean-open Lean Meta Elab
Mathlib/Lean/Name.lean-
Mathlib/Lean/Name.lean:private def isBlackListed (declName : Name) : CoreM Bool := do
Mathlib/Lean/Name.lean-  if declName.toString.startsWith "Lean" then return true
Mathlib/Lean/Name.lean-  let env ← getEnv
Mathlib/Lean/Name.lean-  pure $ declName.isInternal'
Mathlib/Lean/Name.lean-   || isAuxRecursor env declName
Mathlib/Lean/Name.lean-   || isNoConfusion env declName
Mathlib/Lean/Name.lean-  <||> isRec declName <||> isMatcher declName
--
Mathlib/Tactic/Find.lean--- from Lean.Server.Completion
Mathlib/Tactic/Find.lean:private def isBlackListed (declName : Name) : MetaM Bool := do
Mathlib/Tactic/Find.lean-  let env ← getEnv
Mathlib/Tactic/Find.lean-  pure $ declName.isInternal
Mathlib/Tactic/Find.lean-   || isAuxRecursor env declName
Mathlib/Tactic/Find.lean-   || isNoConfusion env declName
Mathlib/Tactic/Find.lean-  <||> isRec declName
Mathlib/Tactic/Find.lean-  <||> isMatcher declName

They seem to be all just a very slightly bit different (filtering out Lean. or not, CoreM vs. MetaM).