Zulip Chat Archive

Stream: general

Topic: unnecessary(?) simp lemma


view this post on Zulip Yury G. Kudryashov (May 01 2020 at 17:39):

I wonder why submodule.map_subtype_top is not reported by lint.

view this post on Zulip Yury G. Kudryashov (May 01 2020 at 17:40):

The proof is by simp

view this post on Zulip Gabriel Ebner (May 01 2020 at 17:44):

We have quite a few of these "short-circuiting" lemmas. It's not redundant because simp will actually use map_subtype_top preferentially. The lemmas used to prove it are not redundant because the don't follow from map_subtype_top.

view this post on Zulip Yury G. Kudryashov (May 01 2020 at 18:01):

Thank you for the explanation.


Last updated: May 15 2021 at 23:13 UTC