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