sig
  type term = LogtkHOTerm.t
  type rule = LogtkHORewriting.term * LogtkHORewriting.term
  exception IllFormedRule of LogtkHORewriting.rule
  type t
  val empty : LogtkHORewriting.t
  val add : LogtkHORewriting.t -> LogtkHORewriting.rule -> LogtkHORewriting.t
  val merge : LogtkHORewriting.t -> LogtkHORewriting.t -> LogtkHORewriting.t
  module Seq :
    sig
      val of_seq :
        LogtkHORewriting.t ->
        LogtkHORewriting.rule Sequence.t -> LogtkHORewriting.t
      val to_seq : LogtkHORewriting.t -> LogtkHORewriting.rule Sequence.t
    end
  val of_list : LogtkHORewriting.rule list -> LogtkHORewriting.t
  val to_list : LogtkHORewriting.t -> LogtkHORewriting.rule list
  val pp : Buffer.t -> t -> unit
  val to_string : t -> string
  val fmt : Format.formatter -> t -> unit
  val cmp : t -> t -> int
  val eq : t -> t -> bool
  val hash_fun : t -> int64 -> int64
  val hash : t -> int
  val normalize :
    LogtkHORewriting.t -> LogtkHORewriting.term -> LogtkHORewriting.term
  val normalize_collect :
    LogtkHORewriting.t ->
    LogtkHORewriting.term ->
    LogtkHORewriting.term * LogtkHORewriting.rule list
end