simp priority

Stream: general

[Scott Morrison]

Does priority actually work with simp?

[Scott Morrison]

I can't find much evidence in the library...

[Scott Morrison]

Oh, I take that back. Changing priorities in category_theory/adjunctions/basic.lean really does break things. :-)

[Floris van Doorn]

I tested some stuff today, and it seems to work, yes.

[Floris van Doorn]

Oh, in reaction to what you said in #1471: it sounds right that simp will simplify subexpressions first, so that the priority won't help in that case.
I tested with 2 simp-lemmas that had the same LHS (but different type-class arguments), and in that case, the priority setting seems to differentiate which lemma is applied.