Topic: simp priority
Scott Morrison (Sep 24 2019 at 04:31):
priority actually work with
Scott Morrison (Sep 24 2019 at 04:32):
I can't find much evidence in the library...
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. :-)
Floris van Doorn (Sep 24 2019 at 05:26):
I tested some stuff today, and it seems to work, yes.
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