Topic: simp_nf failure?
Mario Carneiro (Aug 16 2020 at 14:17):
On current master, src#classical.not_imp is a simp lemma that can be proven from src#classical.not_forall and src#exists_prop . Does anyone have an idea why the
simp_nf linter doesn't notice? I checked nolints and don't see any obvious reason for it to not be found, but I stumbled on this in #3812 where the only essential difference is that the names of these lemmas have changed.
Gabriel Ebner (Aug 17 2020 at 07:23):
This is because
classical.not_imp is declared after
classical.not_forall. We have quite a few of these short-circuiting simp lemmas.
Last updated: Aug 03 2023 at 10:10 UTC