canonically_linear_ordered_monoid.to_linear_ordered_comm_...

Stream: Is there code for X?

[Junyan Xu]

Does the second example below exist in mathlib as a def? Apparently it doesn't exist as an instance. Does it cause any problem to make it an instance? (Same for the additive versions)

import data.nat.basic

example {α} [canonically_ordered_monoid α] : ordered_comm_monoid α :=
by apply_instance /- succeeds -/

example {α} [canonically_linear_ordered_monoid α] : linear_ordered_comm_monoid α :=
by apply_instance /- fails -/

example {α} [m : canonically_linear_ordered_monoid α] : linear_ordered_comm_monoid α :=
{..m} /- succeeds -/