## Stream: general

### Topic: unnecessary(?) simp lemma

#### Yury G. Kudryashov (May 01 2020 at 17:39):

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

#### Yury G. Kudryashov (May 01 2020 at 17:40):

The proof is by simp

#### 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.

#### Yury G. Kudryashov (May 01 2020 at 18:01):

Thank you for the explanation.

Last updated: May 15 2021 at 23:13 UTC