module Conv: sig .. end
type
val create : unit -> ctx
val copy : ctx -> ctx
val clear : ctx -> unit
val of_simple_term : ctx -> TypedSTerm.t -> Type.t option
convert a simple typed term into a type. The term is assumed to be
closed.
Returns an error message if the term is not a type
val var_of_simple_term : ctx -> TypedSTerm.t Var.t -> Type.t HVar.t
Convert a variable (and its type), and remember the binding.
val fresh_ty_var : ctx -> Type.t HVar.t
Fresh type variable
exception Error
val of_simple_term_exn : ctx -> TypedSTerm.t -> Type.t
Raises Invalid_argument if conversion is impossible
val to_simple_term : ?env:TypedSTerm.t Var.t DBEnv.t -> Type.t -> TypedSTerm.t
convert a type to a prolog term.
env : the current environement for De Bruijn indices