Zulip Chat Archive

Stream: general

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