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