Commit 2023-03-27 22:17 f92bbb9f
View on Github →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.