Commit 2020-04-03 08:24 8af4bb8d

refactor(tactic/lint): split into multiple files (#2299) The lint.lean file is getting too long for me to comfortably navigate. This PR splits the file up into several parts:

• tactic.lint.basic defining the linter structure and the @[linter] and @[nolint] attributes
• tactic.lint.frontend defined the functions to run the linters and the various #lint commands
• The linters are split into three separate files, the simp linters, the type class linters, and the rest.
• tactic.lint imports all of the files above so import tactic.lint still works as before