Commit 2025-03-22 14:46 eb9b7072

View on Github →

chore(*): delete nolint simpNF on lemmas involving 1/0 (#23199) Apparently these lemmas used to give simpNF errors because they couldn't apply. But removing the nolint, running #lint, trying out various examples and checking the #discr_tree_simp_key all give as result that they make sense. So I think we can remove these nolints.

Estimated changes