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.

See also

Term.genvar, Term.variant