sig
  type t =
      Dot of (AAC_matcher.symbol * AAC_matcher.Terms.t * AAC_matcher.Terms.t)
    | Plus of
        (AAC_matcher.symbol * AAC_matcher.Terms.t * AAC_matcher.Terms.t)
    | Sym of (AAC_matcher.symbol * AAC_matcher.Terms.t array)
    | Var of AAC_matcher.var
    | Unit of AAC_matcher.symbol
  val equal_aac :
    AAC_matcher.units -> AAC_matcher.Terms.t -> AAC_matcher.Terms.t -> bool
  type nf_term
  val nf_term_compare :
    AAC_matcher.Terms.nf_term -> AAC_matcher.Terms.nf_term -> int
  val nf_equal :
    AAC_matcher.Terms.nf_term -> AAC_matcher.Terms.nf_term -> bool
  val sprint_nf_term : AAC_matcher.Terms.nf_term -> string
  val term_of_t :
    AAC_matcher.units -> AAC_matcher.Terms.t -> AAC_matcher.Terms.nf_term
  val t_of_term : AAC_matcher.Terms.nf_term -> AAC_matcher.Terms.t
end