Topic: with_top "diamonds"
Chris Hughes (Oct 25 2018 at 07:39):
The following equality isn't
rfl. I think it should be. I tried redefining the instances, because I thought it might have something to do with the issue that stopped
(0 : with_bot nat) = some 0 being definitional, but I couldn't get it to work
example : @with_top.add_monoid ℕ _ = add_comm_monoid.to_add_monoid _ := rfl
Johan Commelin (Oct 27 2018 at 05:06):
Hmmm, since when is
(0 : with_bot nat) = some 0 no longer defeq? I know that things like that worked for
with_zero a couple of weeks ago. You are just using a wrapper around
option and the obvious coercion. This seems a bit surprising.
Chris Hughes (Oct 27 2018 at 08:57):
Ages ago it didn't work, but it's now fixed.
Johan Commelin (Oct 27 2018 at 08:58):
Chris Hughes (Oct 27 2018 at 11:22):
Found a fix and PRed. #442
Last updated: May 18 2021 at 07:19 UTC