package logtk
-
logtk
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
package logtk
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
val size : t -> intNumber of elements
Add new elements to the ordering, creating a new ordering. They will not be ordered at all w.r.t previous elements.
val is_total : t -> boolIs 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.
val enrich : t -> (elt -> elt -> LogtkComparison.t) -> unitCompare 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.
val compare : t -> elt -> elt -> LogtkComparison.tcompare two elements in the ordering.