Commit 2023-03-27 22:17 f92bbb9f

feat: LinearOrder α extends Ord α (#2858) This PR makes LinearOrder lawfully extend Ord. Since LinearOrder has decidable order relations, we take compare to be compareOfLessAndEq by default for a linear order. Since typeclass synthesis is preferred by structure instances to optparams, this does not create non-defeq diamonds for types which already have a different implementation of Ord. We also add a field compare_eq_compareOfLessAndEq which encodes the lawful quality by demanding equality to the canonical comparison. Motivation: Array functions like min largely use Ord, so this lets us seamlessly use these array functions when we only have a linear order. See zulip.