module Algebra.Preorder ||| Preorder defines a binary relation using the `<=` operatorpublic exportinterface Preorder a where  (<=) : a -> a -> Bool  preorderRefl : {x : a} -> x <= x = True  preorderTrans : {x, y, z : a} -> x <= y = True -> y <= z = True -> x <= z = True ||| Least Upper Bound, replace max using only Preorderexportlub : Preorder a => a -> a -> alub x y = if x <= y then y else x ||| Greatest Lower Bound, replaces min using only Preorderexportglb : Preorder a => a -> a -> aglb x y = if x <= y then x else y ||| Strict less-than using the relation from a preorderpublic export(<) : (Preorder a, Eq a) => a -> a -> Bool(<) x y = x <= y && x /= y ||| The greatest bound of a bounded lattice, we only need to know about preorders howeverpublic exportinterface Preorder a => Top a where  top : a  topAbs : {x : a} -> x <= top = True