`Prop.Option`

The type `_ option`

, equipped with the ordering `None <= Some x`

. This ordering is not a lattice.

`module X : sig ... end`

`type property = X.t option`

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`

.

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