mathlib3
feat(tactic/linter): add decidable_classical linter
#2352

Merged

feat(tactic/linter): add decidable_classical linter #2352

mergify merged 11 commits into master from decidable_eq_linter

feat(tactic/linter): add decidable_classical linter

baac798d

docstring

5f567ad5

cleanup

5af6e98e

fix build, cleanup

cdcb879b

fix test

d3fc2fde

kim-em commented on 2020-04-08

Update src/tactic/lint/type_classes.lean

8c8b15b6

Update src/tactic/lint/type_classes.lean

ce89e741

Update src/tactic/lint/default.lean

9048f52b

Update src/tactic/lint/type_classes.lean

fec0f2d0

kim-em added ready-to-merge

kim-em approved these changes on 2020-04-08

urkud commented on 2020-04-08

Update src/data/dfinsupp.lean

e015c1aa

Merge branch 'master' into decidable_eq_linter

14cdcb4c

mergify merged 55d430ca into master 5 years ago

mergify deleted the decidable_eq_linter branch 5 years ago

Reviewers

kim-em

urkud

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone