package logtk

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
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

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

Orient a list of pairs