Module Glue.MinimalSemiLatticeSource

MinimalSemiLattice converts a semi-lattice to a minimal semi-lattice; that is, it implements leq_join in terms of separate leq and join operations.

Parameters

module P : sig ... end

Signature

Sourcetype property = P.property

The type property must form a partial order, which must satisfy the ascending chain condition: every monotone sequence must eventually stabilize.

Sourceval 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.