mathlib documentation

tactic.lint.simp

Linter for simplification lemmas

This files defines several linters that prevent common mistakes when declaring simp lemmas:

meta def is_simp_eq  :

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  :
( := 200000)declarationtactic (option string)

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.

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.