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.
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.