Yury G. Kudryashov (Jun 11 2019 at 22:45):
Hi, what lemmas can (not) be marked as
@[simp]? In particular, why
arrow_congr_comp_apply in https://github.com/leanprover-community/mathlib/pull/1119/files can't be marked as
Yury G. Kudryashov (Jun 12 2019 at 15:37):
ping in this topic
Floris van Doorn (Jun 12 2019 at 17:19):
You should think of
simp lemmas as reduction lemmas from the LHS to the RHS. In particular, given an instance of an LHS I need to know what expression (the RHS) it will reduce to. This is not the case for your lemma, since
eb occurs in the RHS, but not in the LHS.
Yury G. Kudryashov (Jun 12 2019 at 18:53):
@Floris van Doorn Thank you for the explanation!
Last updated: May 08 2021 at 05:14 UTC