sig
  type t = TypedSTerm.term
  type builtin = Prop | TType | Term | Int | Rat
  type view =
      Builtin of TypedSTerm.Ty.builtin
    | Var of TypedSTerm.Ty.t Var.t
    | App of ID.t * TypedSTerm.Ty.t list
    | Fun of TypedSTerm.Ty.t list * TypedSTerm.Ty.t
    | Forall of TypedSTerm.Ty.t Var.t * TypedSTerm.Ty.t
    | Multiset of TypedSTerm.Ty.t
    | Record of (string * TypedSTerm.Ty.t) list *
        TypedSTerm.Ty.t Var.t option
    | Meta of TypedSTerm.meta_var
  val view : TypedSTerm.Ty.t -> TypedSTerm.Ty.view
  val tType : TypedSTerm.Ty.t
  val var :
    ?loc:TypedSTerm.location -> TypedSTerm.Ty.t Var.t -> TypedSTerm.Ty.t
  val var_of_string : ?loc:TypedSTerm.location -> string -> TypedSTerm.Ty.t
  val meta :
    ?loc:TypedSTerm.location -> TypedSTerm.meta_var -> TypedSTerm.Ty.t
  val fun_ :
    ?loc:TypedSTerm.location ->
    TypedSTerm.Ty.t list -> TypedSTerm.Ty.t -> TypedSTerm.Ty.t
  val app :
    ?loc:TypedSTerm.location ->
    ID.t -> TypedSTerm.Ty.t list -> TypedSTerm.Ty.t
  val const : ?loc:TypedSTerm.location -> ID.t -> TypedSTerm.Ty.t
  val forall :
    ?loc:TypedSTerm.location ->
    TypedSTerm.Ty.t Var.t -> TypedSTerm.Ty.t -> TypedSTerm.Ty.t
  val forall_l :
    ?loc:TypedSTerm.location ->
    TypedSTerm.Ty.t Var.t list -> TypedSTerm.Ty.t -> TypedSTerm.Ty.t
  val multiset :
    ?loc:TypedSTerm.location -> TypedSTerm.Ty.t -> TypedSTerm.Ty.t
  val record :
    ?loc:TypedSTerm.location ->
    (string * TypedSTerm.Ty.t) list ->
    rest:TypedSTerm.Ty.t Var.t option -> TypedSTerm.Ty.t
  val record_flatten :
    ?loc:TypedSTerm.location ->
    (string * TypedSTerm.Ty.t) list ->
    rest:TypedSTerm.Ty.t option -> TypedSTerm.Ty.t
  val prop : TypedSTerm.Ty.t
  val int : TypedSTerm.Ty.t
  val rat : TypedSTerm.Ty.t
  val term : TypedSTerm.Ty.t
  val ( ==> ) : TypedSTerm.Ty.t list -> TypedSTerm.Ty.t -> TypedSTerm.Ty.t
  val close_forall : TypedSTerm.Ty.t -> TypedSTerm.Ty.t
  val arity : TypedSTerm.Ty.t -> int * int
  val is_tType : TypedSTerm.Ty.t -> bool
  val is_prop : TypedSTerm.Ty.t -> bool
  val returns : TypedSTerm.Ty.t -> TypedSTerm.Ty.t
  val returns_tType : TypedSTerm.Ty.t -> bool
  val returns_prop : TypedSTerm.Ty.t -> bool
end