Wojciech Różowski c04a83a2e5 refactor: turn dupNamespace into a Lean.Linter (#13708) ... This PR moves the `dupNamespace` linter from the `EnvLinter` framework to the `Lean.Linter` (text linter) framework, upstreaming the code from `mathlib`. Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>		2026-05-12 06:39:08 +00:00
..
examples	feat: lake: hoist compiled configurations (#13683)	2026-05-08 18:00:37 +00:00
tests	refactor: turn dupNamespace into a Lean.Linter (#13708)	2026-05-12 06:39:08 +00:00
.gitattributes
.gitignore
lakefile.toml	feat: lake: cached compressed module artifacts (#12914)	2026-03-16 04:36:19 +00:00
run_clean.sh	test: tests/lake/run_test.sh (#13501)	2026-04-25 04:36:08 +00:00
run_test.sh	test: tests/lake/run_test.sh (#13501)	2026-04-25 04:36:08 +00:00