Zulip Chat Archive

Stream: general

Topic: Requirement for being @[simp]


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 @[simp]?

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: Dec 20 2023 at 11:08 UTC