Safe Haskell | Safe-Inferred |
---|---|
Language | GHC2021 |
Documentation
class PEq t => POrd t where Source #
Total ordering relation.
Laws
#<=
must form a total order. More precisely:
x #<= x
=
pcon PTrue
(reflexivity)(y #< x) #|| (z #< y) #|| (x #<= z)
=
pcon PTrue
(transitivity)(x #<= y) #|| (y #<= x)
=
pcon PTrue
(totality)
Furthermore, #<
must be an equivalent strict total order to #<=
:
x #< x
=
pcon PFalse
(irreflexivity)(y #<= x) #|| (z #<= y) #|| (x #< z)
=
pcon PTrue
(transitivity)(x #< y) #|| (y #< x) #|| (x #== z)
=
pcon PTrue
(trichotomy)x #<= y
=
(x #< y) #|| (x #== y)
(strict equivalence)
If you define pmax
or pmin
, ensure the following also hold:
pmax # x # y
=
pmax # y # x
(commutativity, also for @pmin)pmax # x #$ pmax y z
=
pmax # (pmax # x # y) # z
(associativity, also for @pmin)pmax # x #$ pmin # y # z
=
pmin # (pmax # x # y) # (pmax # x # z)
(pmax
distributes overpmin
, also equivalent forpmin
)pmin x y
=
pif' (x #<= y) x y
pmax x y
=
pif' (x #<= y) y x
Laws 8-12 hold if you use the defaults provided by this type class.
@since WIP
Nothing
(#<=) :: Term s t -> Term s t -> Term s PBool infix 4 Source #
@since WIP
(#<) :: Term s t -> Term s t -> Term s PBool infix 4 Source #
@since WIP
pmax :: forall (s :: S). Term s t -> Term s t -> Term s t Source #
@since WIP
pmin :: forall (s :: S). Term s t -> Term s t -> Term s t Source #
@since WIP