1(* ========================================================================= *) 2(* THE KNUTH-BENDIX TERM ORDERING *) 3(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *) 4(* ========================================================================= *) 5 6signature KnuthBendixOrder = 7sig 8 9(* ------------------------------------------------------------------------- *) 10(* The weight of all constants must be at least 1, and there must be at most *) 11(* one unary function with weight 0. *) 12(* ------------------------------------------------------------------------- *) 13 14type kbo = 15 {weight : Term.function -> int, 16 precedence : Term.function * Term.function -> order} 17 18val default : kbo 19 20val compare : kbo -> Term.term * Term.term -> order option 21 22end 23