linear ordered whut?

Stream: general

[Johan Commelin]

import algebra.ordered_field

instance foo (K : Type*) [linear_ordered_field K] :
  linear_ordered_comm_ring K := by apply_instance
-- fails

[Johan Commelin]

/me whut?

[Gabriel Ebner]

It's time to unbundle the decidability assumptions:

instance foo (K : Type*) [discrete_linear_ordered_field K] :
  decidable_linear_ordered_comm_ring K := by apply_instance