Skip to content

[Merged by Bors] - feat: make the dupNamespace linter catch any duplicate namespace(s)#39793

Closed
grunweg wants to merge 33 commits into
leanprover-community:masterfrom
grunweg:dupnamespace-stronger
Closed

[Merged by Bors] - feat: make the dupNamespace linter catch any duplicate namespace(s)#39793
grunweg wants to merge 33 commits into
leanprover-community:masterfrom
grunweg:dupnamespace-stronger

chore(CategoryTheory/Limits/Shapes/Pullback/HasPullback): fix depreca…

2e7d275
Select commit
Loading
Failed to load commit list.
Sign in for the full log view
Verify Transient and Automated Commits
succeeded Jul 1, 2026 in 38s