sig
  type t
  type id
  type location
  val eq_t : Ast_tptp.Term.t
  val neq_t : Ast_tptp.Term.t
  val not_t : Ast_tptp.Term.t
  val or_t : Ast_tptp.Term.t
  val and_t : Ast_tptp.Term.t
  val xor_t : Ast_tptp.Term.t
  val nor_t : Ast_tptp.Term.t
  val nand_t : Ast_tptp.Term.t
  val equiv_t : Ast_tptp.Term.t
  val implies_t : Ast_tptp.Term.t
  val implied_t : Ast_tptp.Term.t
  val data_t : Ast_tptp.Term.t
  val colon :
    ?loc:Ast_tptp.Term.location ->
    Ast_tptp.Term.t -> Ast_tptp.Term.t -> Ast_tptp.Term.t
  val var :
    ?loc:Ast_tptp.Term.location -> Ast_tptp.Term.id -> Ast_tptp.Term.t
  val const :
    ?loc:Ast_tptp.Term.location -> Ast_tptp.Term.id -> Ast_tptp.Term.t
  val distinct :
    ?loc:Ast_tptp.Term.location -> Ast_tptp.Term.id -> Ast_tptp.Term.t
  val int : ?loc:Ast_tptp.Term.location -> string -> Ast_tptp.Term.t
  val rat : ?loc:Ast_tptp.Term.location -> string -> Ast_tptp.Term.t
  val real : ?loc:Ast_tptp.Term.location -> string -> Ast_tptp.Term.t
  val apply :
    ?loc:Ast_tptp.Term.location ->
    Ast_tptp.Term.t -> Ast_tptp.Term.t list -> Ast_tptp.Term.t
  val ite :
    ?loc:Ast_tptp.Term.location ->
    Ast_tptp.Term.t -> Ast_tptp.Term.t -> Ast_tptp.Term.t -> Ast_tptp.Term.t
  val union :
    ?loc:Ast_tptp.Term.location ->
    Ast_tptp.Term.t -> Ast_tptp.Term.t -> Ast_tptp.Term.t
  val product :
    ?loc:Ast_tptp.Term.location ->
    Ast_tptp.Term.t -> Ast_tptp.Term.t -> Ast_tptp.Term.t
  val arrow :
    ?loc:Ast_tptp.Term.location ->
    Ast_tptp.Term.t -> Ast_tptp.Term.t -> Ast_tptp.Term.t
  val subtype :
    ?loc:Ast_tptp.Term.location ->
    Ast_tptp.Term.t -> Ast_tptp.Term.t -> Ast_tptp.Term.t
  val pi :
    ?loc:Ast_tptp.Term.location ->
    Ast_tptp.Term.t list -> Ast_tptp.Term.t -> Ast_tptp.Term.t
  val letin :
    ?loc:Ast_tptp.Term.location ->
    Ast_tptp.Term.t list -> Ast_tptp.Term.t -> Ast_tptp.Term.t
  val forall :
    ?loc:Ast_tptp.Term.location ->
    Ast_tptp.Term.t list -> Ast_tptp.Term.t -> Ast_tptp.Term.t
  val exists :
    ?loc:Ast_tptp.Term.location ->
    Ast_tptp.Term.t list -> Ast_tptp.Term.t -> Ast_tptp.Term.t
  val lambda :
    ?loc:Ast_tptp.Term.location ->
    Ast_tptp.Term.t list -> Ast_tptp.Term.t -> Ast_tptp.Term.t
  val choice :
    ?loc:Ast_tptp.Term.location ->
    Ast_tptp.Term.t list -> Ast_tptp.Term.t -> Ast_tptp.Term.t
  val description :
    ?loc:Ast_tptp.Term.location ->
    Ast_tptp.Term.t list -> Ast_tptp.Term.t -> Ast_tptp.Term.t
  val sequent :
    ?loc:Ast_tptp.Term.location ->
    Ast_tptp.Term.t list -> Ast_tptp.Term.t list -> Ast_tptp.Term.t
end