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
algebra/group.lean and suddenly there is breakage in
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_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