logtk

Core types and algorithms for logic
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library logtk.solving
type term = Logtk.TypedSTerm.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

val orient_lpo_list : (term * term) list -> Constraint.t list

Orient a list of pairs