Commit 2020-02-04 12:42 c5febb52
View on Github →feat(tactic/lint): Three new linters, update illegal_constants (#1947)
- add three new linters
- fix failing declarations
- restrict and rename illegal_constants linter
- update doc
- update ge_or_gt test
- update mk_nolint
- fix error
- Update scripts/mk_nolint.lean Co-Authored-By: Rob Lewis Rob.y.lewis@gmail.com
- Update src/meta/expr.lean Co-Authored-By: Rob Lewis Rob.y.lewis@gmail.com
- clarify unfolds_to_class
- fix names since name is no longer protected also change one declaration back to instance, since it did not cause a linter failure
- fix errors, move notes to docstrings
- add comments to docstring
- update mk_all.sh
- fix linter errors