Up  Next

Module TypedSTerm.Ty

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