Decidable.EqOrd

Provides a type for proving compatibility between Eq and Ord

Definitions

data EqOrdCompat : Bool -> Ordering -> Type

  Compatibility between Eq and Ord

Totality: total
Visibility: public export
Constructors:

LT : EqOrdCompat False LT

GT : EqOrdCompat False GT

EQ : EqOrdCompat True EQ

interface OrdCompatible : Type -> Type

  Types with compatible Eq and Ord instances

Parameters: x
Constraints: Ord x
Methods:

eqOrdCompat : (a : x) -> (b : x) -> EqOrdCompat (a == b) (compare a b)

Implementations:

OrdCompatible ()

OrdCompatible Bool

OrdCompatible Nat

eqOrdCompat : {auto __con : OrdCompatible x} -> (a : x) -> (b : x) -> EqOrdCompat (a == b) (compare a b)

Visibility: public export

eqOrdCompatSucc : EqOrdCompat (a == b) (compare a b) -> EqOrdCompat (S a == S b) (compare (S a) (S b))

Visibility: public export