## Stream: maths

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

Ok, good!

#### Chris Hughes (Oct 27 2018 at 11:22):

Found a fix and PRed. #442

Last updated: May 18 2021 at 07:19 UTC