gen_tyvar
Type.gen_tyvar : unit -> hol_type
Generate a fresh type variable.
An invocation gen_tyvar() generates a type variable tyv not seen in
the current session. Furthermore, the concrete syntax of tyv is such
that tyv is not obtainable by mk_vartype, or by parsing.
Failure
Never fails.
Example
> gen_tyvar();
val it = “:%%gen_tyvar%%30”: hol_type
> try Type `:%%gen_tyvar%%1`;
Exception- HOL_ERR
(at Parse.parse_type: on line 1, characters 11-12:
Type parsing failure with remaining input: %%gen_tyvar%%1) raised
> try mk_vartype "%%gen_tyvar%%1";
val it = “:%%gen_tyvar%%1”: hol_type
Comments
In general, the actual name returned by gen_tyvar should not be relied
on.
Useful for coding some proof procedures.