Skip to main content

LinearOrder

typeclass L: LinearOrder extends PartialOrder {
totality(a: L, b: L) {
a <= b or b <= a
}
}

A linear order (total order) is a partial order where all elements are comparable.

GitHub


antisymmetric​

Inherited from PartialOrder.

gt​

Inherited from PartialOrder.

gte​

Inherited from PartialOrder.

lt​

Inherited from PartialOrder.

lte​

Inherited from LTE.

max​

define max(self, other: L) -> L {
if other <= self {
self
} else {
other
}
}

Yields the larger of two elements.

min​

define min(self, other: L) -> L {
if self <= other {
self
} else {
other
}
}

Yields the smaller of two elements.

reflexive​

Inherited from PartialOrder.

totality​

totality(a: L, b: L) {
a <= b or b <= a
}

All elements are comparable: for any two elements a and b, either a ≤ b or b ≤ a.

transitive​

Inherited from PartialOrder.