## Stream: general

### Topic: What should be @[simp]?

#### Yufan Lou (Feb 24 2020 at 04:34):

I put @[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

• only lemma or theorem, not to def
• only things of the form foo = bar or 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