mathlib
55d430ca - feat(tactic/linter): add decidable_classical linter (#2352)

Commit
5 years ago
feat(tactic/linter): add decidable_classical linter (#2352) * feat(tactic/linter): add decidable_classical linter * docstring * cleanup * fix build, cleanup * fix test * Update src/tactic/lint/type_classes.lean Co-Authored-By: Scott Morrison <scott@tqft.net> * Update src/tactic/lint/type_classes.lean Co-Authored-By: Scott Morrison <scott@tqft.net> * Update src/tactic/lint/default.lean Co-Authored-By: Scott Morrison <scott@tqft.net> * Update src/tactic/lint/type_classes.lean Co-Authored-By: Scott Morrison <scott@tqft.net> * Update src/data/dfinsupp.lean Co-Authored-By: Yury G. Kudryashov <urkud@urkud.name> Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au> Co-authored-by: Scott Morrison <scott@tqft.net> Co-authored-by: Yury G. Kudryashov <urkud@urkud.name> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
Author
Parents
Loading