# Commit 2021-01-04 23:56 12921e9e

View on Github →feat(tactic/simps): some improvements (#5541)

`@[simps]`

would previously fail if the definition is not a constructor application (with the suggestion to add option`{rhs_md := semireducible}`

and maybe`simp_rhs := tt`

). Now it automatically adds`{rhs_md := semireducible, simp_rhs := tt}`

whenever it reaches this situation.- Remove all (now) unnecessary occurrences of
`{rhs_md := semireducible}`

from the library. There are still a couple left where the`simp_rhs := tt`

is undesirable. `@[simps {simp_rhs := tt}]`

now also applies`dsimp, simp`

to the right-hand side of the lemmas it generates.- Add some
`@[simps]`

in`category_theory/limits/cones.lean`

`@[simps]`

would not recursively apply projections of`prod`

or`pprod`

. This is now customizable with the`not_recursive`

option.- Add an option
`trace.simps.debug`

with some debugging information.