Commit 2025-04-15 05:27 593c38c6
View on Github →chore: rename fields of LinearOrder (#23976)
Renames LinearOrder.decidable** -> LinearOrder.toDecidable**, and same for ConditionallyCompleteLinearOrder and CompleteLinearOrder
See zulip message [#mathlib4 > extending `RCLike` and `LinearOrder` @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/extending.20.60RCLike.60.20and.20.60LinearOrder.60/near/511047785)
Also fixes lots of potential diamonds caused by not specifying the decidableEq or decidableLT fields when creating an instance.