Stream: general

Topic: dsimp

Kenny Lau (Apr 21 2018 at 07:14):

So dsimp uses all simp lemmas proved by rfl?

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 11 2021 at 12:15 UTC