Agda.Utils.PartialOrd

data PartialOrdering

leqPO

oppPO

orPO

seqPO

fromOrdering

fromOrderings

toOrderings

Comparison with partial result

type Comparable a

class PartialOrd a

comparableOrd

related

Totally ordered types.

Generic partially ordered types.

data Pointwise a

data Inclusion a

PartialOrdering is itself partially ordered!

Properties

data ISet

prop_comparable_related

prop_oppPO

sortUniq

prop_leqPO_sound

prop_orPO_sound

prop_associative_orPO

prop_commutative_orPO

prop_idempotent_orPO

prop_zero_orPO

property_seqPO

prop_seqPO

prop_identity_seqPO

prop_zero_seqPO

prop_associative_seqPO

prop_commutative_seqPO

prop_idempotent_seqPO

prop_distributive_seqPO_orPO

prop_sorted_toOrderings

prop_toOrderings_after_fromOrdering

prop_fromOrderings_after_toOrderings

prop_toOrderings_after_fromOrderings

prop_related_pair

prop_comparable_PartialOrdering

All tests

tests