Showing changes from revision #7 to #8:
Added | Removed | Changed
A binary relation over a type is a strict order (also called strict total order, strict linear order, or pseudo-order) if it comes with
a family of dependent terms
representing the irreflexivity condition for the binary relation
a family of dependent terms
representing the comparison condition for the binary relation
a family of dependent terms
representing the connectedness condition for the binary relation
a family of dependent terms
representing the asymmetry condition for the binary relation
is called a strictly ordered type.