refactor: turn dupNamespace into a Lean.Linter#13708

wkrozowski merged 1 commit into

leanprover:masterleanprover/lean4:masterfrom

wkrozowski:dupNamespace-linterwkrozowski/lean4:dupNamespace-linterCopy head branch name to clipboard