Skip to main content

JoinSemilattice

typeclass S: JoinSemilattice extends PartialOrder, Join {
    lte_join_left(a: S, b: S) {
        a <= a.join(b)
    }
    lte_join_right(a: S, b: S) {
        b <= a.join(b)
    }
    join_lte_of_bounds(a: S, b: S, c: S) {
        a <= c and b <= c implies a.join(b) <= c
    }
}

A partially ordered type with binary least upper bounds.

GitHub

antisymmetric​

Inherited from PartialOrder.

gt​

Inherited from PartialOrder.

gte​

Inherited from PartialOrder.

join​

Inherited from Join.

join_lte_of_bounds​

join_lte_of_bounds(a: S, b: S, c: S) {
    a <= c and b <= c implies a.join(b) <= c
}

A join is below any common upper bound.

lt​

Inherited from PartialOrder.

lte​

Inherited from LTE.

lte_join_left​

lte_join_left(a: S, b: S) {
    a <= a.join(b)
}

A join is above its left argument.

lte_join_right​

lte_join_right(a: S, b: S) {
    b <= a.join(b)
}

A join is above its right argument.

reflexive​

Inherited from PartialOrder.

transitive​

Inherited from PartialOrder.