Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-02-24 15:43 0fc45dcd

View on Github →

feat(tactic/lint): support @[nolint unused_arguments] (#2041)

  • feat(tactic/lint): support @[nolint unused_arguments]
  • refactor(scripts/mk_nolint): include failing linter name in nolints.txt
  • chore(scripts/nolints): update nolints.txt
  • doc(category/functor): add docstrings

Estimated changes

modified def functor.const
modified def pell.pell
modified theorem filter.mem_at_top_sets
modified def algebra.comap
modified def cardinal.ord_eq_min
modified def ordinal.div_def
modified theorem tactic.interactive.{u}
modified def bar.foo