mathlib3
29079ba8 - feat(tactic/lint): linter improvements (#9901)

Commit
4 years ago
feat(tactic/lint): linter improvements (#9901) * Make the linter framework easier to use on projects outside mathlib with the new `lint_project` (replacing `lint_mathlib`). Also replace `lint_mathlib_decls` by `lint_project_decls`. * Make most declarations in the frontend not-private (I want to use them in other projects) * The unused argument linter does not report declarations that contain `sorry`. It will still report declarations that use other declarations that contain sorry. I did not add a test for this, since it's hard to do that while keeping the test suite silent (but I did test locally). * Some minor changes in the test suite (not important, but they cannot hurt).
Author
Parents
Loading