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