Zulip Chat Archive
Stream: general
Topic: dsimp
Kenny Lau (Apr 21 2018 at 07:14):
So dsimp uses all simp lemmas proved by rfl?
Mario Carneiro (Apr 21 2018 at 07:15):
yes
Mario Carneiro (Apr 21 2018 at 07:15):
it's also a bit more powerful in the places it can rewrite because it's definitional
Mario Carneiro (Apr 21 2018 at 07:16):
but I recommend using simp over dsimp when you can because it decreases reliance on definitional equality
Last updated: May 02 2025 at 03:31 UTC