1\DOC gen_tyvar 2 3\TYPE {gen_tyvar : unit -> hol_type} 4 5\SYNOPSIS 6Generate a fresh type variable. 7 8\KEYWORDS 9variable, type. 10 11\LIBRARY 12Type 13 14\DESCRIBE 15An invocation {gen_tyvar()} generates a type variable {tyv} not 16seen in the current session. Furthermore, the concrete syntax 17of {tyv} is such that {tyv} is not obtainable by {mk_vartype}, 18or by parsing. 19 20\FAILURE 21Never fails. 22 23\EXAMPLE 24{ 25- gen_tyvar(); 26> val it = `:%%gen_tyvar%%1` : hol_type 27 28- try Type `:%%gen_tyvar%%1`; 29 30Exception raised at Parse.hol_type parser: 31Couldn't make any sense with remaining input of "%%gen_tyvar%%1" 32 33- try mk_vartype "%%gen_tyvar%%1"; 34 35Exception raised at Type.mk_vartype: 36incorrect syntax 37} 38 39 40\COMMENTS 41In general, the actual name returned by {gen_tyvar} should not be 42relied on. 43 44\USES 45Useful for coding some proof procedures. 46 47\SEEALSO 48Term.genvar, Term.variant. 49\ENDDOC 50