
  0 | module Algebra.Preorder
  1 | 
  2 | %default total
  3 | 
  4 | ||| Preorder defines a binary relation using the `<=` operator
  5 | public export
  6 | interface Preorder a where
  7 |   (<=) : a -> a -> Bool
  8 |   preorderRefl : {x : a} -> x <= x = True
  9 |   preorderTrans : {x, y, z : a} -> x <= y = True -> y <= z = True -> x <= z = True
 10 | 
 11 | ||| Least Upper Bound, replace max using only Preorder
 12 | export
 13 | lub : Preorder a => a -> a -> a
 14 | lub x y = if x <= y then y else x
 15 | 
 16 | ||| Greatest Lower Bound, replaces min using only Preorder
 17 | export
 18 | glb : Preorder a => a -> a -> a
 19 | glb x y = if x <= y then x else y
 20 | 
 21 | ||| Strict less-than using the relation from a preorder
 22 | public export
 23 | (<) : (Preorder a, Eq a) => a -> a -> Bool
 24 | (<) x y = x <= y && x /= y
 25 | 
 26 | ||| The greatest bound of a bounded lattice, we only need to know about preorders however
 27 | public export
 28 | interface Preorder a => Top a where
 29 |   top : a
 30 |   topAbs : {x : a} -> x <= top = True
 31 |