Topic: What should be @[simp]?
Yufan Lou (Feb 24 2020 at 04:34):
@[simp] on my leftpad definition to demonstrate it, but it definitely cannot be applied to everything. Are there any rules to which I can refer?
Johan Commelin (Feb 24 2020 at 04:46):
Rules of thumb:
@[simp] should be applied to
theorem, not to
- only things of the form
foo = baror
xyzzy = quux
- only if the LHS is "more complex" and the RHS is "simpler"
Johan Commelin (Feb 24 2020 at 04:47):
There are exceptions to these rules, and also the rules are maybe not complete. But they give the rough idea.
Yufan Lou (Feb 24 2020 at 05:00):
now to go back and rewrite my proof :upside_down:
Floris van Doorn (Feb 24 2020 at 18:52):
You can also add
@[simp] to definitions. This will tell
simp that it can unfold this definition.
Scott Morrison (Feb 24 2020 at 20:13):
:up: Use with caution!
If you're defining a structure, you should use
@[simps] in preference to
@[simp], as this defines
simp lemmas for each of the structure projections, but doesn't allow unfolding the entire definition.
Last updated: May 14 2021 at 12:18 UTC