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.

meta def is_simp_eq (a b : expr) :

Checks whether two expressions are equal for the simplifier. That is, they are reducibly-definitional equal, and they have the same head symbol.

meta def simp_nf_linter (timeout : ℕ := 200000) (d : declaration) :

Reports declarations that are simp lemmas whose left-hand side is not in simp-normal form.

meta def linter.simp_nf :

A linter for simp lemmas whose lhs is not in simp-normal form, and which hence never fire.

meta def linter.simp_var_head :

A linter for simp lemmas whose lhs has a variable as head symbol, and which hence never fire.

meta def linter.simp_comm :

A linter for commutativity lemmas that are marked simp.