Reapply "chore(Tactic/Lint/Simp): make simpNF linter dsimp-aware (#839)" (#841)

leanprover-community / batteries

The "batteries included" extended library for the Lean programming language and theorem prover

Apache License 2.0

232 stars 95 forks source link

Reapply "chore(Tactic/Lint/Simp): make simpNF linter dsimp-aware (#839)" (#841) #844

Closed jcommelin closed 2 months ago

jcommelin commented 2 months ago

This reverts commit 0f5b28745722ab5f5168d2a418cabf8bee98f97a.

By now, all problems in mathlib should be fixed, except for one, which seems to be linked to leanprover/lean4#2867. I suggest that we nolint this exception, with a comment pointing to this issue.

The following PR to mathlib4 passes CI and demonstrates the changes required to mathlib4 to appease the dsimpNF linter:

testing new dsimpNF linter leanprover-community/mathlib4#13855