with_top "diamonds"

Stream: maths

[Chris Hughes]

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]

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]

Ages ago it didn't work, but it's now fixed.

[Johan Commelin]

Ok, good!

[Chris Hughes]

Found a fix and PRed. #442