Linter for simplification lemmas #
This files defines several linters that prevent common mistakes when declaring simp lemmas:
simp_nf checks that the left-hand side of a simp lemma is not simplified by a different lemma.
simp_var_head checks that the head symbol of the left-hand side is not a variable.
simp_comm checks that commutativity lemmas are not marked as simplification lemmas.