Fix.MINIMAL_SEMI_LATTICE

type property

val leq_join : property -> property -> property

leq_join p q must compute the join of p and q. If the result is logically equal to q, then q itself must be returned. Thus, we have leq_join p q == q if and only if leq p q holds.

leq_join p q

p

q

leq_join p q == q

leq p q