functor (T : BaseTypes->
  sig
    type symbol = T.symbol
    type var = T.var
    type sort = T.sort
    type attr = T.attr
    type lambda_node = private L of sort list * t
    and lambda = private (lambda_node, unit) Hashcons.hash_consed
    and t_node = private
        FreeVar of var
      | BoundVar of int
      | Leaf of symbol
      | Node of symbol * t list
      | Let of lambda * t list
      | Exists of lambda
      | Forall of lambda
      | Annot of t * attr
    and t_prop = private { bound_vars : int list; }
    and t = private (t_node, t_prop) Hashcons.hash_consed
    and flat = private
        Var of var
      | Const of symbol
      | App of symbol * t list
      | Attr of t * attr
    val compare : t -> t -> int
    val equal : t -> t -> bool
    val hash : t -> int
    val tag : t -> int
    val mk_lambda : var list -> t -> lambda
    val eval_lambda : lambda -> t list -> t
    val partial_eval_lambda : lambda -> t list -> lambda
    val mk_term : t_node -> t
    val mk_var : var -> t
    val mk_const : symbol -> t
    val mk_app : symbol -> t list -> t
    val mk_let : (var * t) list -> t -> t
    val mk_let_elim : (var * t) list -> t -> t
    val mk_exists : var list -> t -> t
    val mk_forall : var list -> t -> t
    val mk_annot : t -> attr -> t
    val node_of_t : t -> t_node
    val node_of_lambda : lambda -> lambda_node
    val sorts_of_lambda : lambda -> sort list
    val tag_of_t : t -> int
    val eval_t :
      ?fail_on_quantifiers:bool -> (flat -> 'a list -> 'a) -> t -> 'a
    val map : (int -> t -> t) -> t -> t
    val destruct : t -> flat
    val has_quantifier : t -> bool
    val instantiate : lambda -> t list -> t
    val construct : flat -> t
    val import : t -> t
    val import_lambda : lambda -> lambda
    val pp_print_term : ?db:int -> Format.formatter -> t -> unit
    val pp_print_lambda_w :
      (?arity:int -> Format.formatter -> symbol -> unit) ->
      (Format.formatter -> var -> unit) ->
      (Format.formatter -> sort -> unit) ->
      ?db:int -> Format.formatter -> lambda -> unit
    val pp_print_term_w :
      (?arity:int -> Format.formatter -> symbol -> unit) ->
      (Format.formatter -> var -> unit) ->
      (Format.formatter -> sort -> unit) ->
      ?db:int -> Format.formatter -> t -> unit
    val print_term : ?db:int -> t -> unit
    val pp_print_lambda : ?db:int -> Format.formatter -> lambda -> unit
    val print_lambda : ?db:int -> lambda -> unit
    val stats : unit -> int * int * int * int * int * int
  end