#### logtk 2.1 2.0 1.6 1.5.1 0.8.1

Core types and algorithms for logic
IN THIS PACKAGE
Module . .

### Constraints

`type 'a t = private ID.t -> ID.t -> int constraint 'a = [< `partial | `total ]`

A partial order on symbols, used to make the precedence more precise. `'a` encodes the kind of ordering: partial or total NOTE: the ordering must partition the set of ALL symbols into equivalence classes, within which all symbols are equal, but symbols of distinct equivalence classes are always ordered.

`type prec_fun = signature:Signature.t -> ID.t Iter.t -> [ `partial ] t`
`val arity : prec_fun`

decreasing arity constraint (big arity => high in precedence)

`val invfreq : prec_fun`

symbols with high frequency are smaller. Elements of unknown frequency are assumed to have a frequency of 0.

`val max : prec_fun`

maximal symbols, in decreasing order

`val min : prec_fun`

minimal symbols, in decreasing order

`val prec_fun_of_str : string -> prec_fun`
`val alpha : [ `total ] t`

alphabetic ordering on symbols, themselves bigger than builtin

`val compose : [ `partial ] t -> [< `partial | `total ] as 'a t -> 'a t`

`compose a b` uses `a` to compare symbols; if `a` cannot decide, then we use `b`.

`val compose_sort : (int * [ `partial ] t) list -> [ `partial ] t`

`compose_sort l` sorts the list by increasing priority (the lower, the earlier an ordering is applied, and therefore the more impact it has) before composing

`val compare_by : constr:'a t -> ID.t -> ID.t -> int`

```compare_by ~constr a b returns the result of comparing symbols a and b using constr```

`val make : ( ID.t -> ID.t -> int ) -> [ `partial ] t`

Create a new partial order. CAUTION, this order must respect some properties (see `'at`)