Module Prop.Boolean

The lattice of Booleans.

The Boolean lattice. The ordering is false <= true.

type property = bool

The type property must form a partial order, and must be equipped with a least element bottom and with an equality test equal. The partial order must satisfy the ascending chain condition: every monotone sequence must eventually stabilize.

We do not require an ordering test leq or a join operation join.

val bottom : property

bottom is the least property.

val equal : property -> property -> bool

equal p q determines whether the properties p and q are equal. In the implementation of this test, it is permitted to assume that p <= q holds.

val is_maximal : property -> bool

is_maximal p determines whether the property p is maximal with respect to the partial order. A conservative check suffices: it is always permitted for is_maximal p to be false. If is_maximal p is true, then p must have no strict upper bound. In particular, if properties form a lattice, then is_maximal p = true implies that p is the top element of the lattice.

val leq : bool -> bool -> bool

leq p q determines whether p <= q holds.

val join : bool -> bool -> bool

join p q is the least upper bound of the properties p and q.

val leq_join : bool -> bool -> bool

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.