Module TypedSTerm.Ty

type t = term
type builtin =
| Prop
| TType
| Term
| Int
| Rat
| Real
type view =
| Ty_builtin of builtin
| Ty_var of t Var.t
| Ty_app of ID.t * t list
| Ty_fun of t list * t
| Ty_forall of t Var.t * t
| Ty_multiset of t
| Ty_record of (string * t) list * t Var.t option
| Ty_meta of meta_var
val view : t -> view
include Interfaces.HASH with type t := t
include Interfaces.EQ
type t
val equal : t -> t -> bool
val hash : t -> int
include Interfaces.ORD with type t := t
type t
val compare : t -> t -> int
val tType : t
val var : ?⁠loc:location -> t Var.t -> t
val var_of_string : ?⁠loc:location -> string -> t
val meta : ?⁠loc:location -> meta_var -> t
val fun_ : ?⁠loc:location -> t list -> t -> t
val app : ?⁠loc:location -> ID.t -> t list -> t
val const : ?⁠loc:location -> ID.t -> t
val forall : ?⁠loc:location -> t Var.t -> t -> t
val forall_l : ?⁠loc:location -> t Var.t list -> t -> t
val multiset : ?⁠loc:location -> t -> t
val record : ?⁠loc:location -> (string * t) list -> rest:t Var.t option -> t
val record_flatten : ?⁠loc:location -> (string * t) list -> rest:t option -> t
val prop : t
val int : t
val rat : t
val real : t
val real : t
val term : t
val (==>) : t list -> t -> t

alias for fun_

val close_forall : t -> t
val unfold : t -> t Var.t list * t list * t

unfold [forall a b. x y z -> ret] returns the triples [a,b], [x,y,z], ret

val arity : t -> int * int

arity ty returns (n,m) where ty = forall x1..xn (a1 ... am -> ret)

val mangle : t -> string

String usable as an identifier, without whitespace

val needs_args : t -> bool

needs_args ty means that arity ty <> (0,0)

val is_quantifier_free : t -> bool

true iff it contains no "forall ty"

val is_prenex : t -> bool

true iff prenex quantification only

val is_tType : t -> bool
val is_prop : t -> bool
val returns : t -> t
val returns_tType : t -> bool
val returns_prop : t -> bool