Lift a decidable relation to an Ordering
,
assuming that incomparable terms are Ordering.eq
.
Equations
Instances For
Construct an Ordering
from a type with a decidable LT
instance,
assuming that incomparable terms are Ordering.eq
.
Lift a decidable relation to an Ordering
,
assuming that incomparable terms are Ordering.eq
.
Construct an Ordering
from a type with a decidable LT
instance,
assuming that incomparable terms are Ordering.eq
.