Lift a decidable relation to an Ordering
,
assuming that incomparable terms are Ordering.eq
.
Instances For
Construct an Ordering
from a type with a decidable LT
instance,
assuming that incomparable terms are Ordering.eq
.
Mathlib.Init.Data.Ordering.Basic
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
.