sig
  type key
  type db_index
  type term = private
      Bound of Term.db_index
    | Variable of Term.key * Variable.t
    | Constant of Term.key * Constant.t
    | Application of Term.key * Term.term * Term.term
    | Abstraction of Term.key * Variable.t * Term.term
  val term_equal : Term.term -> Term.term -> bool
  val term_compare : Term.term -> Term.term -> int
  val term_hash : Term.term -> int
  val is_variable : Term.term -> bool
  val variable : Variable.t -> Term.term
  val is_constant : Term.term -> bool
  val constant : Constant.t -> Term.term
  val constant_value : Term.term -> Constant.t
  val is_symbolic_constant : Term.term -> bool
  val symbolic_constant : Symbol.t -> Term.term
  val symbolic_value : Term.term -> Symbol.t
  val is_integer_constant : Term.term -> bool
  val integer_constant : Big_int.big_int -> Term.term
  val integer_value : Term.term -> Big_int.big_int
  val is_rational_constant : Term.term -> bool
  val rational_constant : Num.num -> Term.term
  val rational_value : Term.term -> Num.num
  val is_application : Term.term -> bool
  val application : Term.term -> Term.term -> Term.term
  val application_function : Term.term -> Term.term
  val application_argument : Term.term -> Term.term
  val binary_application : Term.term -> Term.term -> Term.term -> Term.term
  val ternary_application :
    Term.term -> Term.term -> Term.term -> Term.term -> Term.term
  val nary_application : Term.term -> Term.term list -> Term.term
  val nary_application_decomposition :
    Term.term -> Term.term * Term.term list
  val is_abstraction : Term.term -> bool
  val abstraction : Variable.t -> Term.term -> Term.term
  val nary_abstraction : Variable.t list -> Term.term -> Term.term
  val beta_normal_form : Term.term -> Term.term
  module Term_compared :
    sig
      type t = term
      val equal : t -> t -> bool
      val hash : t -> int
      val compare : t -> t -> int
    end
  module Term_hashtbl :
    sig
      type key = term
      type 'a t
      val create : int -> 'a t
      val clear : 'a t -> unit
      val copy : 'a t -> 'a t
      val add : 'a t -> key -> 'a -> unit
      val remove : 'a t -> key -> unit
      val find : 'a t -> key -> 'a
      val find_all : 'a t -> key -> 'a list
      val replace : 'a t -> key -> 'a -> unit
      val mem : 'a t -> key -> bool
      val iter : (key -> 'a -> unit) -> 'a t -> unit
      val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
      val length : 'a t -> int
    end
  module Term_set :
    sig
      type elt = term
      type t
      val empty : t
      val is_empty : t -> bool
      val mem : elt -> t -> bool
      val add : elt -> t -> t
      val singleton : elt -> t
      val remove : elt -> t -> t
      val union : t -> t -> t
      val inter : t -> t -> t
      val diff : t -> t -> t
      val compare : t -> t -> int
      val equal : t -> t -> bool
      val subset : t -> t -> bool
      val iter : (elt -> unit) -> t -> unit
      val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
      val for_all : (elt -> bool) -> t -> bool
      val exists : (elt -> bool) -> t -> bool
      val filter : (elt -> bool) -> t -> t
      val partition : (elt -> bool) -> t -> t * t
      val cardinal : t -> int
      val elements : t -> elt list
      val min_elt : t -> elt
      val max_elt : t -> elt
      val choose : t -> elt
      val split : elt -> t -> t * bool * t
    end
  module Term_mutable_set :
    sig
      type elt = term
      type t
      val create : unit -> t
      val size : t -> int
      val is_empty : t -> bool
      val mem : t -> elt -> bool
      val add : t -> elt -> unit
      val remove : t -> elt -> unit
      val clear : t -> unit
      val iter : (elt -> unit) -> t -> unit
      val iter_const : ('a -> elt -> unit) -> 'a -> t -> unit
      val fold : ('a -> elt -> 'a) -> 'a -> t -> 'a
      val fold_const : ('a -> 'b -> elt -> 'b) -> 'a -> 'b -> t -> 'b
    end
  module Term_map :
    sig
      type key = term
      type +'a t
      val empty : 'a t
      val is_empty : 'a t -> bool
      val add : key -> 'a -> 'a t -> 'a t
      val find : key -> 'a t -> 'a
      val remove : key -> 'a t -> 'a t
      val mem : key -> 'a t -> bool
      val iter : (key -> 'a -> unit) -> 'a t -> unit
      val map : ('a -> 'b) -> 'a t -> 'b t
      val mapi : (key -> 'a -> 'b) -> 'a t -> 'b t
      val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
      val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
      val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
    end
  module Term_union_find :
    sig
      type elem = term
      type t
      val create : unit -> t
      val equivalent : t -> elem -> elem -> bool
      val union : t -> elem -> elem -> unit
      val representative : t -> elem -> elem
      val is_representative : t -> elem -> bool
      val members : t -> elem -> elem Bunch.t
    end
  val uninterpret :
    (Term.term -> bool) ->
    Term.term Term.Term_hashtbl.t -> Term.term -> Term.term
  val free_variables : Term.term -> Term.Term_set.t
  val string_of_term : Term.term -> string
  val pp_print_term : Format.formatter -> Term.term -> unit
  val print_term : Term.term -> unit
  val pp_compact_print_term : Format.formatter -> Term.term -> unit
  val compact_print_term : Term.term -> unit
  val log_term : int -> Term.term -> unit
end

---

Hosted by the ^* web site.
^*Other names and brands may be claimed as the property of others.