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
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