Zulip Chat Archive

Stream: general

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: Dec 20 2023 at 11:08 UTC