Lean4
/-- Checks if there are declarations in the current file in the namespace `{str}.Simps` that are
not used. -/
def checkForUnusedCustomProjs (stx : Syntax) (str : Name) (projs : Array ParsedProjectionData) : CoreM Unit := do
let nrCustomProjections := projs.toList.countP (·.isCustom)
let env ← getEnv
let customDeclarations :=
env.constants.map₂.foldl (init := #[]) fun xs nm _ =>
if (str ++ `Simps).isPrefixOf nm && !nm.isInternalDetail && !isReservedName env nm then xs.push nm else xs
if nrCustomProjections < customDeclarations.size then
Linter.logLintIf linter.simpsUnusedCustomDeclarations stx
m! "\
Not all of the custom declarations {customDeclarations} are used. Double check the \
spelling, and use `?` to get more information."
