Ord.dk

T : (a : Base.type) -> Type.
Cons : (a : Base.type) -> (Base.El a -> Base.El a -> Ordering.T) -> T a.
def compare : (a : Base.type) -> T a -> Base.El a -> Base.El a -> Ordering.T.
[f] compare _ (Cons _ f) --> f.

def impliesEq : (a : Base.type) -> T a -> Eq.T a.
[a, comp] impliesEq a (Cons _ comp) --> Eq.Cons a (x => y => Ordering.eq (comp x y) Ordering.EQ).

def max : (a : Base.type) -> T a -> Base.El a -> Base.El a -> Base.El a.
private max_aux : (a : Base.type) -> Ordering.T -> Base.El a -> Base.El a -> Base.El a.
[a, f, x, y] max a (Cons _ f) x y --> max_aux a (f x y) x y.
[y] max_aux _ Ordering.LT _ y --> y.
[x] max_aux _ Ordering.EQ x _ --> x.
[x] max_aux _ Ordering.GT x _ --> x.

def gt (a : Base.type) (O : T a) (x : Base.El a) (y : Base.El a) : Bool.T := Ordering.eq (compare a O x y) Ordering.GT.