dupNamespace — Mathlib

Lean4
@[inherit_doc linter.dupNamespace]
def dupNamespace : Linter where
  run :=
    withSetOptionIn fun stx ↦ do
      if getLinterValue linter.dupNamespace (← getLinterOptions) then
        let mut aliases := #[]
        if let some exp := stx.find? (·.isOfKind `Lean.Parser.Command.export) then
          aliases ← getAliasSyntax exp
        for id in (← getNamesFrom (stx.getPos?.getD default)) ++ aliases do
          let declName := id.getId
          if declName.hasMacroScopes || isPrivateName declName then
            continue
          let nm := declName.components
          let some (dup, _) := nm.zip (nm.tailD []) |>.find? fun (x, y) ↦ x == y |
            continue
          Linter.logLint linter.dupNamespace id
              m! "The namespace '{dup }' is duplicated in the declaration '{declName}'"
Похожие утверждения