## Stream: general

### Topic: rfl lemmas

#### Kenny Lau (Sep 05 2018 at 18:50):

how important are rfl-simp-lemmas being rfl?

#### Chris Hughes (Sep 05 2018 at 19:05):

I don't understand the question. You mean how important is it that they're proved using rfl, or that they can be proved using rfl or something completely different?

#### Kenny Lau (Sep 05 2018 at 19:07):

should we depend on rfl lemmas being rfl (so that we can use dsimp instead of simp)?

#### Scott Morrison (Sep 06 2018 at 04:35):

Yes, it's important... I think the point is that dsimp just changes the goal, while simp has to actually construct the proof, and sometimes that goes wrong. I should be able to be more specific (as someone explaining to me this difference actually made a big difference in the behaviour of tidy), but I'm having trouble thinking of an example now.

Last updated: May 15 2021 at 22:14 UTC