logtk.solving
Lpo.FO
logtk
logtk.parsers
logtk.proofs
type term = Logtk.Term.t
val orient_lpo : term -> term -> Constraint.t
orient a b generates a constraint that is sufficient for a to be bigger than b in LPO orderings satisfying the constraints
orient a b
a
b
val orient_lpo_list : (term * term) list -> Constraint.t list
Orient a list of pairs