Quelle KnuthBendixOrder.sig Sprache: unbekannt

(* ========================================================================= *)
(* THE KNUTH-BENDIX TERM ORDERING                                            *)
(* Copyright (c) 2002 Joe Leslie-Hurd, distributed under the BSD License     *)
(* ========================================================================= *)

signature KnuthBendixOrder =
sig

(* ------------------------------------------------------------------------- *)
(* The weight of all constants must be at least 1, and there must be at most *)
(* one unary function with weight 0.                                         *)
(* ------------------------------------------------------------------------- *)

type kbo =
     {weight : Term.function -> int,
      precedence : Term.function * Term.function -> order}

val default : kbo

val compare : kbo -> Term.term * Term.term -> order option

end

Quelle KnuthBendixOrder.sig Sprache: unbekannt

[ Dauer der Verarbeitung: 0.21 Sekunden (vorverarbeitet) ]