Algebra.Preorder

Definitions

interface Preorder : Type -> Type

  Preorder defines a binary relation using the `<=` operator

Parameters: a
Methods:

(<=) : a -> a -> Bool

Fixity Declaration: infix operator, level 6

preorderRefl : x <= x = True

preorderTrans : x <= y = True -> y <= z = True -> x <= z = True

Implementation: 

Preorder ZeroOneOmega

(<=) : Preorder a => a -> a -> Bool

Totality: total
Visibility: public export
Fixity Declaration: infix operator, level 6

preorderRefl : {auto __con : Preorder a} -> x <= x = True

Totality: total
Visibility: public export

preorderTrans : {auto __con : Preorder a} -> x <= y = True -> y <= z = True -> x <= z = True

Totality: total
Visibility: public export

lub : Preorder a => a -> a -> a

  Least Upper Bound, replace max using only Preorder

Totality: total
Visibility: export

glb : Preorder a => a -> a -> a

  Greatest Lower Bound, replaces min using only Preorder

Totality: total
Visibility: export

(<) : (Preorder a, Eq a) => a -> a -> Bool

  Strict less-than using the relation from a preorder

Totality: total
Visibility: public export
Fixity Declaration: infix operator, level 6

interface Top : Type -> Type

  The greatest bound of a bounded lattice, we only need to know about preorders however

Parameters: a
Constraints: Preorder a
Methods:

top : a

topAbs : x <= top = True

Implementation: 

Top ZeroOneOmega

top : Top a => a

Totality: total
Visibility: public export

topAbs : {auto __con : Top a} -> x <= top = True

Totality: total
Visibility: public export