What should be @[simp]?

Stream: general

[Yufan Lou]

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]

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]

There are exceptions to these rules, and also the rules are maybe not complete. But they give the rough idea.

[Yufan Lou]

now to go back and rewrite my proof :upside_down:

[Floris van Doorn]

You can also add @[simp] to definitions. This will tell simp that it can unfold this definition.

[Scott Morrison]

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