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