localDefinitionDependencies — Mathlib

Lean4
/-- Does the declaration with this name depend on definitions in the current file?

Here, "definition" means everything that is not a theorem, and so includes `def`,
`structure`, `inductive`, etc.
-/
def localDefinitionDependencies (env : Environment) (stx id : Syntax) : CommandElabM Bool := do
  let declName ← getDeclName stx
  let immediateDeps ← getAllDependencies stx id
  let immediateDeps : NameSet :=
    immediateDeps.foldl (init := ∅) fun s n => if (env.find? n).isSome then s.insert n else s
  let deps ← liftCoreM <| immediateDeps.transitivelyUsedConstants
  let constInfos := deps.toList.filterMap env.find?
  let defs := constInfos.filter (fun constInfo => !(constInfo matches .thmInfo _ | .ctorInfo _))
  return defs.any fun constInfo => declName != constInfo.name && constInfo.name.isLocal env
Похожие утверждения