Linter for simplification lemmas #
This files defines several linters that prevent common mistakes when declaring simp lemmas:
simpNF
checks that the left-hand side of a simp lemma is not simplified by a different lemma.simpVarHead
checks that the head symbol of the left-hand side is not a variable.simpComm
checks that commutativity lemmas are not marked as simplification lemmas.
Given the list of hypotheses, is this a conditional rewrite rule?
Equations
- One or more equations did not get rendered due to their size.
- Std.Tactic.Lint.isConditionalHyps lhs [] = pure false
Instances For
Runs the continuation on all the simp theorems encoded in the given type.
Instances For
Constructs a message from all the simp theorems encoded in the given type.
Instances For
Returns true if this is a @[simp]
declaration.
Instances For
Returns the list of elements in the discrimination tree.
Instances For
Returns the list of elements in the trie.
Add message msg
to any errors thrown inside k
.
Instances For
Render the list of simp lemmas.
Instances For
A linter for simp lemmas whose lhs is not in simp-normal form, and which hence never fire.
Instances For
A linter for simp lemmas whose lhs has a variable as head symbol, and which hence never fire.
Instances For
A linter for commutativity lemmas that are marked simp.