module Stdlib.Trait.Ord;

open import Stdlib.Data.Bool.Base;

type Ordering :=
  | LT : Ordering
  | EQ : Ordering
  | GT : Ordering;

isLT : Ordering → Bool;
isLT LT := true;
isLT _ := false;

isEQ : Ordering → Bool;
isEQ EQ := true;
isEQ _ := false;

isGT : Ordering → Bool;
isGT GT := true;
isGT _ := false;

--- A trait for defining a total order
type Ord (A : Type) :=
  | mkOrd : (A -> A -> Ordering) -> Ord A;