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.
Reports declarations that are simp lemmas whose left-hand side is not in simp-normal form.
A linter for simp lemmas whose lhs is not in simp-normal form, and which hence never fire.
A linter for simp lemmas whose lhs has a variable as head symbol, and which hence never fire.