sig
  type t
  type id
  type location
  val eq_t : Term_intf.Logic.t
  val neq_t : Term_intf.Logic.t
  val wildcard : Term_intf.Logic.t
  val tType : Term_intf.Logic.t
  val prop : Term_intf.Logic.t
  val true_ : Term_intf.Logic.t
  val false_ : Term_intf.Logic.t
  val not_t : Term_intf.Logic.t
  val or_t : Term_intf.Logic.t
  val and_t : Term_intf.Logic.t
  val xor_t : Term_intf.Logic.t
  val nor_t : Term_intf.Logic.t
  val nand_t : Term_intf.Logic.t
  val equiv_t : Term_intf.Logic.t
  val implied_t : Term_intf.Logic.t
  val implies_t : Term_intf.Logic.t
  val data_t : Term_intf.Logic.t
  val var :
    ?loc:Term_intf.Logic.location -> Term_intf.Logic.id -> Term_intf.Logic.t
  val const :
    ?loc:Term_intf.Logic.location -> Term_intf.Logic.id -> Term_intf.Logic.t
  val atom : ?loc:Term_intf.Logic.location -> int -> Term_intf.Logic.t
  val distinct :
    ?loc:Term_intf.Logic.location -> Term_intf.Logic.id -> Term_intf.Logic.t
  val int : ?loc:Term_intf.Logic.location -> string -> Term_intf.Logic.t
  val rat : ?loc:Term_intf.Logic.location -> string -> Term_intf.Logic.t
  val real : ?loc:Term_intf.Logic.location -> string -> Term_intf.Logic.t
  val hexa : ?loc:Term_intf.Logic.location -> string -> Term_intf.Logic.t
  val binary : ?loc:Term_intf.Logic.location -> string -> Term_intf.Logic.t
  val colon :
    ?loc:Term_intf.Logic.location ->
    Term_intf.Logic.t -> Term_intf.Logic.t -> Term_intf.Logic.t
  val eq :
    ?loc:Term_intf.Logic.location ->
    Term_intf.Logic.t -> Term_intf.Logic.t -> Term_intf.Logic.t
  val not_ :
    ?loc:Term_intf.Logic.location -> Term_intf.Logic.t -> Term_intf.Logic.t
  val or_ :
    ?loc:Term_intf.Logic.location ->
    Term_intf.Logic.t list -> Term_intf.Logic.t
  val and_ :
    ?loc:Term_intf.Logic.location ->
    Term_intf.Logic.t list -> Term_intf.Logic.t
  val imply :
    ?loc:Term_intf.Logic.location ->
    Term_intf.Logic.t -> Term_intf.Logic.t -> Term_intf.Logic.t
  val equiv :
    ?loc:Term_intf.Logic.location ->
    Term_intf.Logic.t -> Term_intf.Logic.t -> Term_intf.Logic.t
  val apply :
    ?loc:Term_intf.Logic.location ->
    Term_intf.Logic.t -> Term_intf.Logic.t list -> Term_intf.Logic.t
  val ite :
    ?loc:Term_intf.Logic.location ->
    Term_intf.Logic.t ->
    Term_intf.Logic.t -> Term_intf.Logic.t -> Term_intf.Logic.t
  val pi :
    ?loc:Term_intf.Logic.location ->
    Term_intf.Logic.t list -> Term_intf.Logic.t -> Term_intf.Logic.t
  val letin :
    ?loc:Term_intf.Logic.location ->
    Term_intf.Logic.t list -> Term_intf.Logic.t -> Term_intf.Logic.t
  val forall :
    ?loc:Term_intf.Logic.location ->
    Term_intf.Logic.t list -> Term_intf.Logic.t -> Term_intf.Logic.t
  val exists :
    ?loc:Term_intf.Logic.location ->
    Term_intf.Logic.t list -> Term_intf.Logic.t -> Term_intf.Logic.t
  val lambda :
    ?loc:Term_intf.Logic.location ->
    Term_intf.Logic.t list -> Term_intf.Logic.t -> Term_intf.Logic.t
  val choice :
    ?loc:Term_intf.Logic.location ->
    Term_intf.Logic.t list -> Term_intf.Logic.t -> Term_intf.Logic.t
  val description :
    ?loc:Term_intf.Logic.location ->
    Term_intf.Logic.t list -> Term_intf.Logic.t -> Term_intf.Logic.t
  val arrow :
    ?loc:Term_intf.Logic.location ->
    Term_intf.Logic.t -> Term_intf.Logic.t -> Term_intf.Logic.t
  val product :
    ?loc:Term_intf.Logic.location ->
    Term_intf.Logic.t -> Term_intf.Logic.t -> Term_intf.Logic.t
  val union :
    ?loc:Term_intf.Logic.location ->
    Term_intf.Logic.t -> Term_intf.Logic.t -> Term_intf.Logic.t
  val subtype :
    ?loc:Term_intf.Logic.location ->
    Term_intf.Logic.t -> Term_intf.Logic.t -> Term_intf.Logic.t
  val sequent :
    ?loc:Term_intf.Logic.location ->
    Term_intf.Logic.t list -> Term_intf.Logic.t list -> Term_intf.Logic.t
  val annot :
    ?loc:Term_intf.Logic.location ->
    Term_intf.Logic.t -> Term_intf.Logic.t list -> Term_intf.Logic.t
  val sexpr :
    ?loc:Term_intf.Logic.location ->
    Term_intf.Logic.t list -> Term_intf.Logic.t
end