sig
  type symbol = Symbol.t
  type var = Var.t
  type sort = Type.t
  type 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