Mathlib v3 is deprecated. Go to Mathlib v4

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

Estimated changes