Zulip Chat Archive

Stream: general

Topic: understanding simp

Johan Commelin (Feb 26 2019 at 16:05):

I'm baffled. I added

@[simp] lemma with_zero.coe_one [has_one α] : ((1 : α) : with_zero α) = 1 := rfl

to algebra/group.lean and suddenly there is breakage in algebra/ordered_ring.lean because simp is applying that lemma in the context of with_top α. What's going on?

Johan Commelin (Feb 26 2019 at 16:14):

I thought that this simp-lemma wouldn't apply because of the ((1 : α) : with_zero α) on the right-hand-side.

Johan Commelin (Feb 26 2019 at 16:15):

Is this a bad simp-lemma, because the with_zero somehow gets hidden inside a has_coe, and then with_zero and with_top are both defined as option, so they turn out to be defeq, and hence the simp-lemma applies?

Last updated: Aug 03 2023 at 10:10 UTC