module Util (T : S) : sig .. end
type T.t
val ty_exn : T.t -> T.t
val ty_type : T.t
val ty_prop : T.t
val ty_unitype : T.t
val builtin : ?loc:TermTyped.loc -> ty:T.t -> T.t TI.Builtin.t -> T.t
val const : ?loc:TermTyped.loc -> ty:T.t -> TI.id -> T.t
val true_ : T.t
val var : ?loc:TermTyped.loc -> T.t TI.var -> T.t
val app : ?loc:TermTyped.loc -> ty:T.t -> T.t -> T.t list -> T.t
val mk_bind : ?loc:TermTyped.loc -> ty:T.t -> TI.Binder.t -> T.t TI.var -> T.t -> T.t
val fun_ : ?loc:TermTyped.loc -> ty:T.t -> T.t TI.var -> T.t -> T.t
val mu : ?loc:TermTyped.loc -> T.t TI.var -> T.t -> T.t
val let_ : ?loc:TermTyped.loc -> T.t TI.var -> T.t -> T.t -> T.t
val match_with : ?loc:TermTyped.loc -> ty:T.t -> T.t -> T.t TI.cases -> T.t
val ite : ?loc:TermTyped.loc -> T.t -> T.t -> T.t -> T.t
val forall : ?loc:TermTyped.loc -> T.t TI.var -> T.t -> T.t
val exists : ?loc:TermTyped.loc -> T.t TI.var -> T.t -> T.t
val eq : ?loc:TermTyped.loc -> T.t -> T.t -> T.t
val asserting : ?loc:TermTyped.loc -> T.t -> T.t list -> T.t
val ty_builtin : ?loc:TermTyped.loc -> TI.TyBuiltin.t -> T.t
val ty_const : ?loc:TermTyped.loc -> TI.id -> T.t
val ty_var : ?loc:TermTyped.loc -> T.t TI.var -> T.t
val ty_meta_var : ?loc:TermTyped.loc -> T.t MetaVar.t -> T.t
val ty_app : ?loc:TermTyped.loc -> T.t -> T.t list -> T.t
val ty_arrow : ?loc:TermTyped.loc -> T.t -> T.t -> T.t
val ty_arrow_l : ?loc:TermTyped.loc -> T.t list -> T.t -> T.t
val ty_forall : ?loc:TermTyped.loc -> T.t TI.var -> T.t -> T.t
include struct ... end
val is_ty : T.t -> bool