Commit 2022-06-13 19:31 e5f69930

View on Github →

feat: port misc linters (#276)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Group/Defs.lean

Modified Mathlib/Data/Array/Defs.lean

modified def Array.range

Modified Mathlib/Data/List/Basic.lean

added theorem Option.mem_toList

Modified Mathlib/Data/Option/Defs.lean

deleted theorem Option.mem_toList

Modified Mathlib/Init/Data/Nat/Lemmas.lean

deleted theorem Nat.Nat.pow_eq

deleted theorem Nat.Nat.pow_succ'

added theorem Nat.pow_eq

added theorem Nat.pow_succ'

Modified Mathlib/Init/Logic.lean

added theorem Iff.elim

deleted def Iff.elim

added theorem Iff.elim_left

deleted def Iff.elim_left

added theorem Iff.elim_right

deleted def Iff.elim_right

added theorem congr_arg

deleted def congr_arg

added theorem congr_fun

deleted def congr_fun

added theorem eq_rec_heq

deleted def eq_rec_heq

added theorem proof_irrel

deleted def proof_irrel

Modified Mathlib/Lean/NameMapAttribute.lean

Modified Mathlib/Logic/Basic.lean

Modified Mathlib/Tactic/Lint.lean

Modified Mathlib/Tactic/Lint/Basic.lean

modified def Mathlib.Tactic.Lint.shouldBeLinted

Created Mathlib/Tactic/Lint/Misc.lean

added def Mathlib.Tactic.Lint.checkType

added def Mathlib.Tactic.Lint.checkUnivs

added def Mathlib.Tactic.Lint.defLemma

added def Mathlib.Tactic.Lint.docBlame

added def Mathlib.Tactic.Lint.docBlameThm

added def Mathlib.Tactic.Lint.dupNamespace

added def Mathlib.Tactic.Lint.explicitVarsOfIff

added def Mathlib.Tactic.Lint.findUnusedHaves

added def Mathlib.Tactic.Lint.synTaut

added def Mathlib.Tactic.Lint.unusedArguments

added def Mathlib.Tactic.Lint.unusedHavesSuffices

Modified Mathlib/Tactic/Lint/Simp.lean

Modified Mathlib/Testing/SlimCheck/Gen.lean

modified def SlimCheck.Gen.prodOf

Modified Mathlib/Testing/SlimCheck/Sampleable.lean

Modified Mathlib/Testing/SlimCheck/Testable.lean

Modified scripts/nolints.json