mathlib3

feat(tactic/linter): add decidable_classical linter

#2352

Merged