Commit 2024-09-05 20:53 1a5a717b

feat: flexible linter and tests (#11821) A linter for "flexible" tactic. The "flexible" linter makes sure that a "rigid" tactic (such as rw) does not act on the output of a "flexible" tactic (such as simp). This is an evolution of the "non-terminal simp" linter. Zulip threads:

• non-terminal simp
• flexible vs rigid Here is a gist with the linter warnings from a previous run. In #11822, the linter runs on most of mathlib and you can see in the output of CI what issues it flags.