gen_tyvar : unit -> hol_type
STRUCTURE
Type
SYNOPSIS
Generate a fresh type variable.
LIBRARY
Type
DESCRIPTION
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%%1` : hol_type

- try Type `:%%gen_tyvar%%1`;

Exception raised at Parse.hol_type parser:
Couldn't make any sense with remaining input of "%%gen_tyvar%%1"

- try mk_vartype "%%gen_tyvar%%1";

Exception raised at Type.mk_vartype:
incorrect syntax

COMMENTS
In general, the actual name returned by gen_tyvar should not be relied on.
USES
Useful for coding some proof procedures.
SEEALSO
genvar, variant
HOL  Kananaskis-14