Topic: simp being silly again
Reid Barton (May 11 2019 at 11:59):
Is there a reason that
simp could fail to apply a simp lemma, but
rw with that lemma works fine?
simp fails it means I have to apply
erw, but it seems to be getting dumber
Mario Carneiro (May 12 2019 at 06:45):
simp and rw use different ways of rewriting, and this can affect when one can succeed over another. Generally the
congr approach to using rewrite lemmas works better, but there are some locations in a term that are not traversed, while
rw will rewrite everywhere uniformly and hope for the best.
Last updated: Aug 03 2023 at 10:10 UTC