Zulip Chat Archive

Stream: general

Topic: Requirement for being @[simp]


view this post on Zulip 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]?

view this post on Zulip Yury G. Kudryashov (Jun 12 2019 at 15:37):

ping in this topic

view this post on Zulip 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.

view this post on Zulip 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