Zulip Chat Archive

Stream: general

Topic: simp priority


view this post on Zulip Scott Morrison (Sep 24 2019 at 04:31):

Does priority actually work with simp?

view this post on Zulip Scott Morrison (Sep 24 2019 at 04:32):

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

view this post on Zulip Scott Morrison (Sep 24 2019 at 04:34):

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

view this post on Zulip Floris van Doorn (Sep 24 2019 at 05:26):

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

view this post on Zulip Floris van Doorn (Sep 24 2019 at 15:05):

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.


Last updated: May 15 2021 at 22:14 UTC