module Stdlib.Trait.Ord;

import Stdlib.Data.Bool.Base open;

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

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

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

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

--- A trait for defining a total order
trait
type Ord A := mkOrd {cmp : A -> A -> Ordering};