Commit 2024-06-24 10:09 34a88764

View on Github →

feat(lint-style): rewrite the 'broad imports' linters in Lean (#14059) This time, the error codes are intentionally changed, as the old ones feel actively misleading.

Estimated changes