mathlib
fb878e78 - feat(tactic/lint): add linter for simp lemmas whose lhs has a variable as head symbol (#2038)

Commit

6 years ago

feat(tactic/lint): add linter for simp lemmas whose lhs has a variable as head symbol (#2038) Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

References

#2038 - feat(tactic/lint): add linter for simp lemmas whose lhs has a variable as head symbol

Author

gebner

Parents

cb4bdd83

mathlib fb878e78 - feat(tactic/lint): add linter for simp lemmas whose lhs has a variable as head symbol (#2038)

mathlib
fb878e78 - feat(tactic/lint): add linter for simp lemmas whose lhs has a variable as head symbol (#2038)