package logtk

Elements that can be compared

the partial order on elements of type elt

build an empty partial order for the list of elements

Copy of the partial order

Number of elements

Add new elements to the ordering, creating a new ordering. They will not be ordered at all w.r.t previous elements.

Is the ordering total (i.e. each pair of elements it contains is ordered)?

More details than is_total, which returns true iff this function returns `total.

• since 0.6.1

Compare unordered pairs with the given partial order function. If the function returns LogtkComparison.t.Eq on two elements x and y, then the ordering cannot be total anymore.

complete po f completes po using the function f elements to compare still unordered pairs. If f x y returns 0 then x and y are still incomparable in po afterwards. If the given comparison function is not total, the ordering may still not be complete. The comparison function f is assumed to be such that transitive_closure f is a partial order.

compare two elements in the ordering.

list of pairs (a > b)

Elements of the partial order. If the ordering is total, they will be sorted by decreasing order (maximum first)