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