Def Mathlib.Tactic.Lint.unusedHavesSuffices

Modification history

2022-09-04 16:26

Mathlib/Tactic/Lint/Misc.lean

feat: depend on std4 (#397)

Deleted Mathlib.Tactic.Lint.unusedHavesSuffices View on Github →

2022-06-13 19:31

Mathlib/Tactic/Lint/Misc.lean

feat: port misc linters (#276)

Added Mathlib.Tactic.Lint.unusedHavesSuffices View on Github →