Skip to main content

PartialOrder

typeclass P: PartialOrder {
    lte: (P, P) -> Bool
    reflexive {
        is_reflexive(P.lte)
    }
    transitive {
        is_transitive(P.lte)
    }
    antisymmetric {
        is_antisymmetric(P.lte)
    }
}

A partial order is a relation that is reflexive, transitive, and antisymmetric. Not all elements need to be comparable.

GitHub

antisymmetric​

antisymmetric {
    is_antisymmetric(P.lte)
}

The order relation must be antisymmetric: if a ≤ b and b ≤ a, then a = b.

gt​

define gt(self, other: P) -> Bool {
    other < self
}

Strict greater-than comparison.

gte​

define gte(self, other: P) -> Bool {
    other <= self
}

Greater-than-or-equal-to comparison.

lt​

define lt(self, other: P) -> Bool {
    self <= other and self != other
}

Strict less-than comparison.

lte​

lte: (P, P) -> Bool

The less-than-or-equal-to relation defining the partial order.

reflexive​

reflexive {
    is_reflexive(P.lte)
}

The order relation must be reflexive: every element is ≤ itself.

transitive​

transitive {
    is_transitive(P.lte)
}

The order relation must be transitive: if a ≤ b and b ≤ c, then a ≤ c.