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