Module Term

module Term: sig  end

val eq : t -> t -> bool

val eql : t list -> t list -> bool

val mk_var : Name.t -> Dom.t option -> t

val mk_const : Sym.t -> t

val mk_app : Sym.t -> t list -> t

module Hashq: sig  end

val mk_num : Hashq.key -> t

val mk_rename : Name.t -> int option -> Dom.t option -> t

val mk_fresh : Name.t -> int option -> Dom.t option -> t

val mk_slack : int option -> bool -> Dom.t option -> t

val is_rename : t -> bool

val is_fresh : t -> bool

val is_internal : t -> bool

val is_slack : t -> bool

val is_var : t -> bool

val is_app : t -> bool

val is_const : t -> bool

val is_intvar : t -> bool

val is_realvar : t -> bool

val to_var : t -> Var.t

val name_of : t -> Name.t

val destruct : t -> Sym.t * t list

val sym_of : t -> Sym.t

val args_of : t -> t list

val poly_of : t -> Mpa.Q.t * t list

val hash : t -> int

val cmp : t -> t -> int

val cmpl : t list -> t list -> int

val (<<<) : t -> t -> bool

val orient : t * t -> t * t

val min : t -> t -> t

val max : t -> t -> t

val is_interp_const : t -> bool

val is_interp : t -> bool

val is_uninterpreted : t -> bool

val is_equal : t -> t -> Three.t

val mapl : (t -> t) -> t list -> t list

val assq : t -> (t * 'a) list -> 'a

val fold : (t -> 'a -> 'a) -> t -> 'a -> 'a

val iter : (t -> 'a) -> t -> unit

val for_all : (t -> bool) -> t -> bool

val subterm : t -> t -> bool

val occurs : t -> t -> bool

val pretty : bool Pervasives.ref

val pp : t Pretty.printer

val to_string : t -> string

val pp_equal : Format.formatter -> t * t -> unit

val pp_diseq : Format.formatter -> t * t -> unit

module Set: sig  end

module Map: sig  end

val apply : Map.key Map.t -> Map.key -> Map.key

val vars_of : Set.elt -> Set.t