This files defines several linters that prevent common mistakes when declaring simp lemmas:
The hypotheses of the theorem
True if this is a conditional rewrite rule
The thing to replace
The result of replacement
The data associated to a simp theorem.
Given the list of hypotheses, is this a conditional rewrite rule?
Runs the continuation on all the simp theorems encoded in the given type.
Checks whether two expressions are equal for the simplifier. That is,
they are reducibly-definitional equal, and they have the same head symbol.
Constructs a message from all the simp theorems encoded in the given type.
Returns true if this is a @[simp] declaration.
Returns the list of elements in the discrimination tree.
Returns the list of elements in the trie.
Add message msg to any errors thrown inside k.
Render the list of simp lemmas.
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.
A linter for commutativity lemmas that are marked simp.