sig
  type location = ParseLocation.t
  type builtin =
      Wildcard
    | Ttype
    | Prop
    | True
    | False
    | Eq
    | Distinct
    | Ite
    | Sequent
    | Subtype
    | Product
    | Union
    | Not
    | And
    | Or
    | Nand
    | Xor
    | Nor
    | Imply
    | Implied
    | Equiv
  type binder = All | Ex | Pi | Arrow | Let | Fun | Choice | Description
  type descr =
      Symbol of Id.t
    | Builtin of Term.builtin
    | Colon of Term.t * Term.t
    | App of Term.t * Term.t list
    | Binder of Term.binder * Term.t list * Term.t
  and t = {
    term : Term.descr;
    attr : Term.t list;
    loc : Term.location option;
  }
  val eq_t : t
  val neq_t : t
  val wildcard : t
  val tType : t
  val prop : t
  val true_ : t
  val false_ : t
  val not_t : t
  val or_t : t
  val and_t : t
  val xor_t : t
  val nor_t : t
  val nand_t : t
  val equiv_t : t
  val implied_t : t
  val implies_t : t
  val data_t : t
  val var : ?loc:location -> Id.t -> t
  val const : ?loc:location -> Id.t -> t
  val atom : ?loc:location -> int -> t
  val distinct : ?loc:location -> Id.t -> t
  val int : ?loc:location -> string -> t
  val rat : ?loc:location -> string -> t
  val real : ?loc:location -> string -> t
  val hexa : ?loc:location -> string -> t
  val binary : ?loc:location -> string -> t
  val colon : ?loc:location -> t -> t -> t
  val eq : ?loc:location -> t -> t -> t
  val not_ : ?loc:location -> t -> t
  val or_ : ?loc:location -> t list -> t
  val and_ : ?loc:location -> t list -> t
  val imply : ?loc:location -> t -> t -> t
  val equiv : ?loc:location -> t -> t -> t
  val apply : ?loc:location -> t -> t list -> t
  val ite : ?loc:location -> t -> t -> t -> t
  val pi : ?loc:location -> t list -> t -> t
  val letin : ?loc:location -> t list -> t -> t
  val forall : ?loc:location -> t list -> t -> t
  val exists : ?loc:location -> t list -> t -> t
  val lambda : ?loc:location -> t list -> t -> t
  val choice : ?loc:location -> t list -> t -> t
  val description : ?loc:location -> t list -> t -> t
  val arrow : ?loc:location -> t -> t -> t
  val product : ?loc:location -> t -> t -> t
  val union : ?loc:location -> t -> t -> t
  val subtype : ?loc:location -> t -> t -> t
  val sequent : ?loc:location -> t list -> t list -> t
  val annot : ?loc:location -> t -> t list -> t
  val sexpr : ?loc:location -> t list -> t
  val fun_ty : ?loc:Term.location -> Term.t list -> Term.t -> Term.t
  val pp : Buffer.t -> Term.t -> unit
  val print : Format.formatter -> Term.t -> unit
end