mathlib3
feat(tactic/lint): linter for commutativity lemmas that are marked simp
#2045

Merged

feat(tactic/lint): linter for commutativity lemmas that are marked simp #2045

mergify merged 4 commits into master from simp-comm-lint

gebner force pushed from 6bcc9ad9 to 8baa62d5 5 years ago

kim-em approved these changes on 2020-02-25

kim-em added ready-to-merge

feat(tactic/lint): linter for commutativity lemmas that are marked simp

6d8d3920

chore(*): remove simp from commutativity lemmas

55d9ff1d

doc(*): document simp_comm linter

281f5dcb

gebner force pushed from fad25738 to 281f5dcb 5 years ago

Merge branch 'master' into simp-comm-lint

de01d6f3

mergify merged 089d0586 into master 5 years ago

mergify deleted the simp-comm-lint branch 5 years ago

Reviewers

kim-em

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone