Decidable.Ordering

Definitions

data OrdDecides : (0 _ : (a -> a -> Type)) -> a -> a -> Ordering -> Type

Totality: total
Visibility: public export
Constructors:

LT : r x y -> OrdDecides r x y LT

EQ : x = y -> OrdDecides r x y EQ

GT : r y x -> OrdDecides r x y GT

interface DecOrd : (a : Type) -> (a -> a -> Type) -> Type

Parameters: a, r
Constraints: TotalOrder a r, Ord a
Methods:

decOrd : (x : a) -> (y : a) -> OrdDecides r x y (compare x y)

Implementations:

DecOrd Bool BoolOrder

DecOrd Nat LT

(DecOrd a r, DecOrd b s) => DecOrd (Either a b) (EitherOrder r s)

DecOrd a r => DecOrd (List a) (Lexicographic r)

decOrd : {auto __con : DecOrd a r} -> (x : a) -> (y : a) -> OrdDecides r x y (compare x y)

Visibility: public export

ordDecidesEq : {auto {conArg:1366} : (Ord a, Irreflexive a r)} -> OrdDecides r x y (compare x y) -> Dec (x = y)

Visibility: public export

data BoolOrder : Bool -> Bool -> Type

Totality: total
Visibility: public export
Constructor: 

FalseTrue : BoolOrder False True

Hints:

DecOrd Bool BoolOrder

Irreflexive Bool BoolOrder

TotalOrder Bool BoolOrder

Transitive Bool BoolOrder

Trichotomous Bool BoolOrder

decOrdNatSucc : OrdDecides LT m n (compare m n) -> OrdDecides LT (S m) (S n) (compare (S m) (S n))

Visibility: public export