Commit 2024-03-29 04:50 f8bc0b20

feat: dupNamespace as a syntax linter (#11154) An implementation of the dupNamespace from Std as a syntax linter. The linter emits a warning for declarations that have a repeated, consecutive namespace:

• Nat.Nat.foo triggers the linter;
• Nat.foo.Nat does not trigger the linter. Note. This linter will not detect duplication in namespaces of autogenerated declarations (other than the one whose declId is present in the source declaration). Zulip discussion The linter found

private theorem Seminorm.Seminorm.isLUB_sSup ...

that is skipped by the environment dupNamespace linter.