module Stdlib.Trait.Ord;
import Stdlib.Data.Fixity open;
import Stdlib.Data.Bool.Base open;
import Stdlib.Trait.Eq 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;
instance
orderingEqI : Eq Ordering :=
mkEq@{
eq (x : Ordering) : Ordering -> Bool
| LT := isLT x
| EQ := isEQ x
| GT := isGT x
};
--- A trait for defining a total order
trait
type Ord A := mkOrd {cmp : A -> A -> Ordering};
syntax operator <= comparison;
--- Returns ;true; iff the first element is less than or equal to the second.
<= {A} {{Ord A}} (x y : A) : Bool :=
case Ord.cmp x y of
| EQ := true
| LT := true
| GT := false;
syntax operator < comparison;
--- Returns ;true; iff the first element is less than the second.
< {A} {{Ord A}} (x y : A) : Bool :=
case Ord.cmp x y of
| EQ := false
| LT := true
| GT := false;
syntax operator > comparison;
--- Returns ;true; iff the first element is greater than the second.
> {A} {{Ord A}} (x y : A) : Bool := y < x;
syntax operator >= comparison;
--- Returns ;true; iff the first element is greater than or equal to the second.
>= {A} {{Ord A}} (x y : A) : Bool := y <= x;
--- Returns the smaller element.
min {A} {{Ord A}} (x y : A) : A := ite (x < y) x y;
--- Returns the larger element.
max {A} {{Ord A}} (x y : A) : A := ite (x > y) x y;
Last modified on 2024-07-11 16:35 UTC