Skip to main content

DistribLattice

typeclass L: DistribLattice extends Lattice {
meet_join_distrib_left(a: L, b: L, c: L) {
a.meet(b.join(c)) = a.meet(b).join(a.meet(c))
}
join_meet_distrib_left(a: L, b: L, c: L) {
a.join(b.meet(c)) = a.join(b).meet(a.join(c))
}
}

A lattice where meets distribute over joins and joins distribute over meets.

GitHub


antisymmetric​

Inherited from PartialOrder.

gt​

Inherited from PartialOrder.

gte​

Inherited from PartialOrder.

join​

Inherited from Join.

join_lte_of_bounds​

Inherited from JoinSemilattice.

join_meet_distrib_left​

join_meet_distrib_left(a: L, b: L, c: L) {
a.join(b.meet(c)) = a.join(b).meet(a.join(c))
}

Join distributes over meet on the left.

lt​

Inherited from PartialOrder.

lte​

Inherited from LTE.

lte_join_left​

Inherited from JoinSemilattice.

lte_join_right​

Inherited from JoinSemilattice.

lte_meet_of_bounds​

Inherited from MeetSemilattice.

meet​

Inherited from Meet.

meet_join_distrib_left​

meet_join_distrib_left(a: L, b: L, c: L) {
a.meet(b.join(c)) = a.meet(b).join(a.meet(c))
}

Meet distributes over join on the left.

meet_lte_left​

Inherited from MeetSemilattice.

meet_lte_right​

Inherited from MeetSemilattice.

reflexive​

Inherited from PartialOrder.

transitive​

Inherited from PartialOrder.